diff --git a/developers/build-sequence b/developers/build-sequence
index d3928c3779..2c8fa267a2 100644
--- a/developers/build-sequence
+++ b/developers/build-sequence
@@ -107,7 +107,6 @@ pancake/semantics
 pancake/parser
 pancake/static_checker
 pancake/proofs
-pancake/ta_progs
 
 # dafny compiler
 compiler/dafny
diff --git a/pancake/README.md b/pancake/README.md
index c3aa15cedd..62f7a5837a 100644
--- a/pancake/README.md
+++ b/pancake/README.md
@@ -73,20 +73,5 @@ Semantics for Pancake and its intermediate languages.
 [static_checker](static_checker):
 Support files for Pancake static checker
 
-[taParserScript.sml](taParserScript.sml):
-Parser for compactDSL programs
-
-[ta_progs](ta_progs):
-Some sample timed automata (TA) programs.
-
 [temp](temp):
 Temporary files
-
-[timeLangScript.sml](timeLangScript.sml):
-Abstract syntax for timeLang
-
-[time_to_panScript.sml](time_to_panScript.sml):
-Compilation from timeLang to panLang
-
-[time_to_targetScript.sml](time_to_targetScript.sml):
-Compiler from timeLang to machine code
diff --git a/pancake/semantics/compactDSLSemScript.sml b/pancake/semantics/compactDSLSemScript.sml
deleted file mode 100644
index d0ea65f292..0000000000
--- a/pancake/semantics/compactDSLSemScript.sml
+++ /dev/null
@@ -1,260 +0,0 @@
-(*
-  semantics for timeLang
-*)
-
-open preamble
-     timeLangTheory
-
-val _ = new_theory "compactDSLSem";
-
-
-Datatype:
-  label = LDelay time
-        | LAction ioAction
-End
-
-Datatype:
-  state =
-  <| clocks   : clock |-> time
-   ; location : loc
-   ; ioAction : ioAction option
-   ; waitTime : time option
-  |>
-End
-
-
-Definition mkState_def:
-  mkState cks loc io wt =
-  <| clocks   := cks
-   ; location := loc
-   ; ioAction := io
-   ; waitTime := wt
-  |>
-End
-
-Definition resetOutput_def:
-  resetOutput st =
-  st with
-  <| ioAction := NONE
-   ; waitTime := NONE
-  |>
-End
-
-Definition resetClocks_def:
-  resetClocks fm xs =
-    fm |++ ZIP (xs,MAP (λx. 0:time) xs)
-End
-
-
-(*
-Definition resetClocks_def:
-  resetClocks clks cvars_vals =
-    clks |++ MAP (λx. (x,0:time)) cvars_vals
-End
-*)
-
-
-(*
-Definition resetClocks_def:
-  resetClocks (st:state) cvs =
-  let reset_cvs = MAP (λx. (x,0:time)) cvs in
-      st with clocks := st.clocks |++ reset_cvs
-End
-*)
-
-(* TODO: rephrase this def *)
-
-Definition list_min_option_def:
-  (list_min_option ([]:num list) = NONE) /\
-  (list_min_option (x::xs) =
-   case list_min_option xs of
-   | NONE => SOME x
-   | SOME y => SOME (if x < y then x else y))
-End
-
-Definition delay_clocks_def:
-  delay_clocks fm (d:num) = FEMPTY |++
-                            (MAP (λ(x,y). (x,y+d))
-                            (fmap_to_alist fm))
-End
-
-
-Definition minusT_def:
-  minusT (t1:time) (t2:time) = t1 - t2
-End
-
-
-Definition evalExpr_def:
-  evalExpr st e =
-  case e of
-  | ELit t => SOME t
-  | EClock c => FLOOKUP st.clocks c
-  | ESub e1 e2 =>
-      case (evalExpr st e1, evalExpr st e2) of
-      | SOME t1,SOME t2 =>
-                  if t2 ≤ t1 then SOME (minusT t1 t2)
-                  else NONE
-      | _=> NONE
-End
-
-(*
-Definition evalExpr_def:
-  (evalExpr st (ELit t) = t) ∧
-  (evalExpr st (ESub e1 e2) =
-    minusT (evalExpr st e1) (evalExpr st e2)) ∧
-  (evalExpr st (EClock c) =
-    case FLOOKUP st.clocks c of
-     | NONE => 0
-     | SOME t => t)
-End
-*)
-
-(*
-Definition evalCond_def:
-  (evalCond st (CndLe e1 e2) = (evalExpr st e1 <= evalExpr st e2)) /\
-  (evalCond st (CndLt e1 e2) = (evalExpr st e1 < evalExpr st e2))
-End
-*)
-
-Definition evalCond_def:
-  (evalCond st (CndLe e1 e2) =
-    case (evalExpr st e1,evalExpr st e2) of
-    | SOME t1,SOME t2 => t1 ≤ t2
-    | _ => F) ∧
-  (evalCond st (CndLt e1 e2) =
-    case (evalExpr st e1,evalExpr st e2) of
-    | SOME t1,SOME t2 => t1 < t2
-    | _ => F)
-End
-
-
-Definition evalDiff_def:
-  evalDiff st ((t,c): time # clock) =
-    evalExpr st (ESub (ELit t) (EClock c))
-End
-
-
-Definition calculate_wtime_def:
-  calculate_wtime st clks diffs =
-  let
-    st = st with clocks := resetClocks st.clocks clks
-  in
-    list_min_option (MAP (THE o evalDiff st) diffs)
-End
-
-
-Inductive evalTerm:
-  (∀st in_signal cnds clks dest diffs.
-     EVERY (λck. ck IN FDOM st.clocks) clks ∧
-     EVERY (λ(t,c).
-             ∃v. FLOOKUP st.clocks c = SOME v ∧
-                 v ≤ t) diffs ==>
-     evalTerm st (SOME in_signal)
-              (Tm (Input in_signal)
-                  cnds
-                  clks
-                  dest
-                  diffs)
-              (st with  <| clocks   := resetClocks st.clocks clks
-                         ; ioAction := SOME (Input in_signal)
-                         ; location := dest
-                         ; waitTime := calculate_wtime st clks diffs|>)) /\
-  (∀st out_signal cnds clks dest diffs.
-     EVERY (λck. ck IN FDOM st.clocks) clks ∧
-     EVERY (λ(t,c).
-             ∃v. FLOOKUP st.clocks c = SOME v ∧
-                 v ≤ t) diffs ==>
-     evalTerm st NONE
-              (Tm (Output out_signal)
-                  cnds
-                  clks
-                  dest
-                  diffs)
-              (st with  <| clocks   := resetClocks st.clocks clks
-                         ; ioAction := SOME (Output out_signal)
-                         ; location := dest
-                         ; waitTime := calculate_wtime st clks diffs|>))
-End
-
-
-Inductive pickTerm:
-  (* when each condition is true and input signals match with the first term *)
-  (!st cnds in_signal clks dest diffs tms st'.
-    EVERY (λcnd. evalCond st cnd) cnds ∧
-    evalTerm st (SOME in_signal) (Tm (Input in_signal) cnds clks dest diffs) st' ==>
-    pickTerm st (SOME in_signal) (Tm (Input in_signal) cnds clks dest diffs :: tms) st') ∧
-
-  (* when each condition is true and output signals match with the first term *)
-  (!st cnds out_signal clks dest diffs tms st'.
-    EVERY (λcnd. evalCond st cnd) cnds ∧
-    evalTerm st NONE (Tm (Output out_signal) cnds clks dest diffs) st' ==>
-    pickTerm st NONE (Tm (Output out_signal) cnds clks dest diffs :: tms) st') ∧
-
-  (* when any condition is false, but there is a matching term, then we can append the
-     list with the false term  *)
-  (!st cnds event ioAction clks dest diffs tms st'.
-    (* new *)
-    EVERY (λcnd. EVERY (λe. ∃t. evalExpr st e = SOME t) (destCond cnd)) cnds ∧
-    ~(EVERY (λcnd. evalCond st cnd) cnds) ∧
-    pickTerm st event tms st' ==>
-    pickTerm st event (Tm ioAction cnds clks dest diffs :: tms) st') ∧
-
-   (* when the input event does not match, but there is a matching term, then we can append the
-      list with the false term *)
-  (!st cnds event in_signal clks dest diffs tms st'.
-    event <> SOME in_signal ∧
-    pickTerm st event tms st' ==>
-    pickTerm st event (Tm (Input in_signal) cnds clks dest diffs :: tms) st') ∧
-
-  (* we can also append this in case of any SOME event with an output term *)
-  (!st cnds event out_signal clks dest diffs tms st'.
-    event <> NONE ∧
-    pickTerm st event tms st' ==>
-    pickTerm st event (Tm (Output out_signal) cnds clks dest diffs :: tms) st')
-End
-
-
-Inductive step:
-  (!p st d.
-    st.waitTime = NONE ==>
-    step p (LDelay d) st
-         (mkState
-          (delay_clocks (st.clocks) d)
-          st.location
-          NONE
-          NONE)) /\
-
-  (!p st d w.
-    st.waitTime = SOME w ∧
-    d ≤ w ==>
-    step p (LDelay d) st
-         (mkState
-          (delay_clocks (st.clocks) d)
-          st.location
-          NONE
-          (SOME (w - d)))) ∧
-
-  (!p st tms st' in_signal.
-      ALOOKUP p st.location = SOME tms /\
-      pickTerm (resetOutput st) (SOME in_signal) tms st' /\
-      st'.ioAction = SOME (Input in_signal) ==>
-      step p (LAction (Input in_signal)) st st') /\
-(* st has zero wakeup t *)
-  (!p st tms st' out_signal.
-    ALOOKUP p st.location = SOME tms /\
-    pickTerm (resetOutput st) NONE tms st' /\
-    st'.ioAction = SOME (Output out_signal) ==>
-    step p (LAction (Output out_signal)) st st')
-End
-
-
-Inductive stepTrace:
-  (!p st.
-    stepTrace p st st []) /\
-  (!p lbl st st' st'' tr.
-    step p lbl st st' /\
-    stepTrace p st' st'' tr ==>
-    stepTrace p st st'' (lbl::tr))
-End
-
-val _ = export_theory();
diff --git a/pancake/semantics/timeFunSemScript.sml b/pancake/semantics/timeFunSemScript.sml
deleted file mode 100644
index aed30bcbfc..0000000000
--- a/pancake/semantics/timeFunSemScript.sml
+++ /dev/null
@@ -1,644 +0,0 @@
-(*
-  semantics for timeLang
-*)
-
-open preamble
-     timeLangTheory
-     timeSemTheory
-
-val _ = new_theory "timeFunSem";
-
-
-Datatype:
-  input_delay = Delay
-              | Input num
-End
-
-(* a well-formed program will not produce NONE in eval_term *)
-(* now returns (label, state) option *)
-Definition eval_term_def:
-  (eval_term st (SOME i)
-                (Tm (Input in_signal)
-                    cnds
-                    clks
-                    dest
-                    difs) =
-   if i = in_signal ∧
-      EVERY (λck. ck IN FDOM st.clocks) clks ∧
-      EVERY (λ(t,c).
-              ∃v. FLOOKUP st.clocks c = SOME v ∧
-                  v ≤ t) difs
-   then SOME (LAction (Input in_signal),
-              st with  <| clocks   := resetClocks st.clocks clks
-                          ; ioAction := SOME (Input in_signal)
-                          ; location := dest
-                          ; waitTime := calculate_wtime st clks difs|>)
-   else NONE) ∧
-
-  (eval_term st NONE
-                (Tm (Output out_signal)
-                    cnds
-                    clks
-                    dest
-                    difs) =
-   if EVERY (λck. ck IN FDOM st.clocks) clks ∧
-      EVERY (λ(t,c).
-              ∃v. FLOOKUP st.clocks c = SOME v ∧
-                  v ≤ t) difs
-   then SOME (LAction (Output out_signal),
-              st with  <| clocks   := resetClocks st.clocks clks
-                          ; ioAction := SOME (Output out_signal)
-                          ; location := dest
-                          ; waitTime := calculate_wtime st clks difs|>)
-   else NONE) ∧
-  (eval_term st _ _ = NONE)
-End
-
-
-Definition machine_bounds_def:
-  machine_bounds st m tms ⇔
-    tms_conds_eval st tms ∧
-    conds_eval_lt_dimword m st tms ∧
-    terms_time_range m tms ∧
-    input_terms_actions m tms ∧
-    terms_wtimes_ffi_bound m st tms ∧
-    max_clocks st.clocks m
-End
-
-(* now returns (label, state) option *)
-Definition pick_eval_input_term_def:
-  (pick_eval_input_term st i m (tm::tms) =
-   case tm of
-   | Tm (Input in_signal) cnds clks dest difs =>
-       if in_signal = i ∧
-          EVERY (λcnd. evalCond st cnd) cnds
-       then eval_term st (SOME i) tm
-       else pick_eval_input_term st i m tms
-   | _ => pick_eval_input_term st i m tms) ∧
-  (pick_eval_input_term st i m [] =
-   if i + 1 < m then SOME (LPanic (PanicInput i), st)
-   else NONE)
-End
-
-Definition pick_eval_output_term_def:
-  (pick_eval_output_term st (tm::tms) =
-   case tm of
-   | Tm (Output out_signal) cnds clks dest difs =>
-       if EVERY (λcnd. evalCond st cnd) cnds
-       then eval_term st NONE tm
-       else pick_eval_output_term st tms
-   | _ => pick_eval_output_term st tms) ∧
-  (pick_eval_output_term st [] = SOME (LPanic PanicTimeout, st))
-End
-
-
-Definition eval_input_def:
-  eval_input prog m n i st =
-  case ALOOKUP prog st.location of
-  | SOME tms =>
-      if n < m ∧ machine_bounds (resetOutput st) m tms
-      then pick_eval_input_term (resetOutput st) i m tms
-      else NONE
-  | _ => NONE
-End
-
-Definition eval_output_def:
-  eval_output prog m n st =
-  case ALOOKUP prog st.location of
-  | SOME tms =>
-      if n < m ∧ machine_bounds (resetOutput st) m tms
-      then pick_eval_output_term (resetOutput st) tms
-      else NONE
-  | _ => NONE
-End
-
-
-Definition eval_delay_wtime_none_def:
-  eval_delay_wtime_none st m n =
-  if n + 1 < m ∧
-     max_clocks (delay_clocks (st.clocks) (n + 1)) m
-  then SOME
-       (LDelay 1 ,
-        st with
-           <|clocks := delay_clocks (st.clocks) 1;
-             ioAction := NONE|>)
-  else NONE
-End
-
-Definition eval_delay_wtime_some_def:
-  eval_delay_wtime_some st m n w =
-  if 1 ≤ w ∧ w < m ∧ n + 1 < m ∧
-     max_clocks (delay_clocks (st.clocks) (n + 1)) m
-  then SOME
-       (LDelay 1 ,
-        st with
-           <|clocks := delay_clocks (st.clocks) 1;
-             waitTime := SOME (w - 1);
-             ioAction := NONE|>)
-  else NONE
-End
-
-(* rearrange the check on system time *)
-Definition eval_step_def:
-  eval_step prog m n (or:input_delay) st =
-  case st.waitTime of
-  | NONE =>
-      (case or of
-       | Delay => eval_delay_wtime_none st m n
-       | Input i => eval_input prog m n i st)
-  | SOME w =>
-      if w = 0
-      then eval_output prog m n st
-      else
-        (case or of
-         | Delay => eval_delay_wtime_some st m n w
-         | Input i =>
-             if w ≠ 0 ∧ w < m
-             then eval_input prog m n i st
-             else NONE)
-End
-
-
-Definition next_oracle_def:
-  next_oracle (f:num -> input_delay) =
-    λn. f (n+1)
-End
-
-Definition set_oracle_def:
-  (set_oracle (Input _) (or:num -> input_delay) = next_oracle or) ∧
-  (set_oracle (Output _) or = or)
-End
-
-(*
-Definition eval_steps_def:
-  (eval_steps 0 prog m n _ st =
-   if n < m ∧
-      (case st.waitTime of
-       | SOME w => w < m
-       | NONE => T)
-   then SOME ([],[])
-   else NONE) ∧
-  (eval_steps (SUC k) prog m n or st =
-   case eval_step prog m n (or 0) st of
-   | SOME (lbl, st') =>
-       let n' =
-             case lbl of
-             | LDelay d => d + n
-             | _ => n;
-           noracle =
-             case lbl of
-             | LDelay _ => next_oracle or
-             | LAction act => set_oracle act or
-       in
-         (case eval_steps k prog m n' noracle st' of
-          | NONE => NONE
-          | SOME (lbls', sts') => SOME (lbl::lbls', st'::sts'))
-   | NONE => NONE)
-End
-*)
-
-
-Definition eval_steps_def:
-  (eval_steps 0 _ _ _ _ st = SOME ([],[])) ∧
-  (eval_steps (SUC k) prog m n or st =
-   if m - 1 <= n then SOME ([], [])
-   else
-     (case eval_step prog m n (or 0) st of
-      | SOME (lbl, st') =>
-          let n' =
-              case lbl of
-              | LDelay d => d + n
-              | _ => n;
-              noracle =
-              case lbl of
-              | LDelay _ => next_oracle or
-              | LAction act => set_oracle act or
-       in
-         (case eval_steps k prog m n' noracle st' of
-          | NONE => NONE
-          | SOME (lbls', sts') => SOME (lbl::lbls', st'::sts'))
-         | NONE => NONE))
-End
-
-(*
-Definition eval_steps_def:
-  (eval_steps 0 _ _ _ _ st = SOME ([],[])) ∧
-  (eval_steps (SUC k) prog m n or st =
-   case eval_step prog m n (or 0) st of
-   | SOME (lbl, st') =>
-       let n' =
-           case lbl of
-           | LDelay d => d + n
-           | _ => n;
-           noracle =
-           case lbl of
-           | LDelay _ => next_oracle or
-           | LAction act => set_oracle act or
-       in
-         (case eval_steps k prog m n' noracle st' of
-          | NONE => NONE
-          | SOME (lbls', sts') => SOME (lbl::lbls', st'::sts'))
-         | NONE => NONE)
-End
-*)
-
-Theorem label_from_pick_eval_input_term:
-  ∀tms i st lbl st' m.
-    pick_eval_input_term st i m tms = SOME (lbl,st') ⇒
-    lbl = LAction (Input i) ∨
-    lbl = LPanic (PanicInput i)
-Proof
-  Induct >> rw [] >>
-  gvs [pick_eval_input_term_def] >>
-  every_case_tac >> gvs [eval_term_def] >>
-  res_tac >> gvs []
-QED
-
-Theorem label_from_pick_eval_output_term:
-  ∀tms st lbl st'.
-    pick_eval_output_term st tms = SOME (lbl,st') ⇒
-    (∃os. lbl = LAction (Output os)) ∨
-    lbl = LPanic PanicTimeout
-Proof
-  Induct >> rw [] >>
-  gvs [pick_eval_output_term_def] >>
-  every_case_tac >> gvs [eval_term_def] >>
-  res_tac >> gvs []
-QED
-
-
-Theorem pick_eval_input_term_imp_pickTerm:
-  ∀tms st m i st'.
-    machine_bounds (resetOutput st) m tms ∧
-    pick_eval_input_term (resetOutput st) i m tms =
-    SOME (LAction (Input i), st') ⇒
-    pickTerm (resetOutput st) m (SOME i) tms st' (LAction (Input i)) ∧
-    st'.ioAction = SOME (Input i)
-Proof
-  Induct >>
-  rpt gen_tac >>
-  strip_tac >>
-  gs []
-  >- gs [pick_eval_input_term_def] >>
-  gs [pick_eval_input_term_def] >>
-  cases_on ‘h’ >> gs [] >>
-  cases_on ‘i'’ >> gs []
-  >- (
-    FULL_CASE_TAC >> gvs []
-    >- (
-      rewrite_tac [Once pickTerm_cases] >>
-      gs [] >>
-      gs [machine_bounds_def] >>
-      gs [eval_term_def, evalTerm_cases] >>
-      rveq >> gs [state_component_equality]) >>
-    cases_on ‘ n' = i’ >> gvs []
-    >- (
-      rewrite_tac [Once pickTerm_cases] >>
-      gs [] >>
-      last_x_assum (qspecl_then [‘st’, ‘m’, ‘i’, ‘st'’] mp_tac) >>
-      impl_tac
-      >- (
-        gs [] >>
-        gs [machine_bounds_def, tms_conds_eval_def, conds_eval_lt_dimword_def,
-            terms_time_range_def, input_terms_actions_def, terms_wtimes_ffi_bound_def,
-            terms_in_signals_def]) >>
-      strip_tac >>
-      gs [machine_bounds_def, terms_time_range_def,
-          conds_eval_lt_dimword_def, input_terms_actions_def,
-          terms_in_signals_def, tms_conds_eval_def] >>
-      disj2_tac >>
-      gs [tm_conds_eval_def, EVERY_MEM] >>
-      rw [] >> gvs [ timeLangTheory.termConditions_def] >>
-      res_tac >> gvs [] >>
-      FULL_CASE_TAC >> gvs []) >>
-    rewrite_tac [Once pickTerm_cases] >>
-    gs [] >>
-    last_x_assum (qspecl_then [‘st’, ‘m’, ‘i’, ‘st'’] mp_tac) >>
-    impl_tac
-    >- (
-      gs [] >>
-      gs [machine_bounds_def, tms_conds_eval_def, conds_eval_lt_dimword_def,
-          terms_time_range_def, input_terms_actions_def, terms_wtimes_ffi_bound_def,
-          terms_in_signals_def]) >>
-    strip_tac >>
-    gs [machine_bounds_def, terms_time_range_def,
-        conds_eval_lt_dimword_def, input_terms_actions_def,
-        terms_in_signals_def, tms_conds_eval_def,  tm_conds_eval_def,
-        timeLangTheory.termConditions_def] >>
-    gs [EVERY_MEM]) >>
-  rewrite_tac [Once pickTerm_cases] >>
-  gs [] >>
-  last_x_assum (qspecl_then [‘st’, ‘m’, ‘i’, ‘st'’] mp_tac) >>
-  impl_tac
-  >- (
-    gs [] >>
-    gs [machine_bounds_def, tms_conds_eval_def, conds_eval_lt_dimword_def,
-        terms_time_range_def, input_terms_actions_def, terms_wtimes_ffi_bound_def,
-        terms_in_signals_def]) >>
-  strip_tac >>
-  gs [machine_bounds_def, terms_time_range_def,
-      conds_eval_lt_dimword_def, input_terms_actions_def,
-      terms_in_signals_def]
-QED
-
-
-Theorem pick_eval_output_term_imp_pickTerm:
-  ∀tms st m os st'.
-    machine_bounds (resetOutput st) m tms ∧
-    pick_eval_output_term (resetOutput st) tms =
-    SOME (LAction (Output os),st') ⇒
-    pickTerm (resetOutput st) m NONE tms st' (LAction (Output os)) ∧
-    st'.ioAction = SOME (Output os)
-Proof
-  Induct >>
-  rpt gen_tac >>
-  strip_tac >>
-  gs []
-  >- gs [pick_eval_output_term_def] >>
-  gs [pick_eval_output_term_def] >>
-  cases_on ‘h’ >> gs [] >>
-  reverse (cases_on ‘i’) >> gs []
-  >- (
-    FULL_CASE_TAC >> gs [] >> rveq >> gs []
-    >- (
-      rewrite_tac [Once pickTerm_cases] >>
-      gs [] >>
-      gs [machine_bounds_def, terms_time_range_def,
-          conds_eval_lt_dimword_def, input_terms_actions_def,
-          terms_in_signals_def] >>
-      gs [eval_term_def, evalTerm_cases] >>
-      rveq >> gs [state_component_equality]) >>
-    rewrite_tac [Once pickTerm_cases] >>
-    gs [] >>
-    last_x_assum (qspecl_then [‘st’, ‘m’, ‘os’, ‘st'’] mp_tac) >>
-    impl_tac
-    >- (
-      gs [] >>
-      gs [machine_bounds_def, tms_conds_eval_def, conds_eval_lt_dimword_def,
-          terms_time_range_def, input_terms_actions_def, terms_wtimes_ffi_bound_def,
-          terms_in_signals_def]) >>
-    strip_tac >>
-    gs [machine_bounds_def, terms_time_range_def,
-        conds_eval_lt_dimword_def, input_terms_actions_def,
-        terms_in_signals_def, tms_conds_eval_def,  tm_conds_eval_def,
-        timeLangTheory.termConditions_def] >>
-    gs [EVERY_MEM] >>
-    disj2_tac >>
-    rw [] >>
-    res_tac >> gs []  >>
-    FULL_CASE_TAC >> gs []) >>
-  rewrite_tac [Once pickTerm_cases] >>
-  gs [] >>
-  last_x_assum (qspecl_then [‘st’, ‘m’, ‘os’, ‘st'’] mp_tac) >>
-  impl_tac
-  >- (
-    gs [] >>
-    gs [machine_bounds_def, tms_conds_eval_def, conds_eval_lt_dimword_def,
-        terms_time_range_def, input_terms_actions_def, terms_wtimes_ffi_bound_def,
-        terms_in_signals_def]) >>
-  strip_tac >>
-  gs [machine_bounds_def, terms_time_range_def,
-      conds_eval_lt_dimword_def, input_terms_actions_def,
-      terms_in_signals_def, tms_conds_eval_def,  tm_conds_eval_def,
-      timeLangTheory.termConditions_def]
-QED
-
-Theorem pick_input_term_panic_sts_eq:
-  ∀tms st m i st'.
-    pick_eval_input_term st i m tms =
-    SOME (LPanic (PanicInput i), st') ⇒
-    st = st'
-Proof
-  Induct >>
-  rpt gen_tac >>
-  strip_tac >>
-  gs [pick_eval_input_term_def] >>
-  every_case_tac >> gvs [eval_term_def] >>
-  res_tac >> gvs []
-QED
-
-Theorem pick_eval_input_term_panic_imp_pickTerm:
-  ∀tms st m i st'.
-    machine_bounds (resetOutput st) m tms ∧
-    pick_eval_input_term (resetOutput st) i m tms =
-    SOME (LPanic (PanicInput i), st') ⇒
-    pickTerm (resetOutput st) m (SOME i) tms st' (LPanic (PanicInput i))
-Proof
-  Induct >>
-  rpt gen_tac >>
-  strip_tac >>
-  gs []
-  >- (
-    gs [pick_eval_input_term_def] >>
-    rewrite_tac [Once pickTerm_cases] >>
-    gs [machine_bounds_def]) >>
-  gs [pick_eval_input_term_def] >>
-  cases_on ‘h’ >> gs [] >>
-  cases_on ‘i'’ >> gs []
-  >- (
-    FULL_CASE_TAC >> gs []
-    >- (
-      rewrite_tac [Once pickTerm_cases] >>
-      gs [] >>
-      gvs [machine_bounds_def] >>
-      gs [eval_term_def, evalTerm_cases] >>
-      rveq >> gs [state_component_equality]) >>
-    cases_on ‘ n' = i’ >> gvs []
-    >- (
-      rewrite_tac [Once pickTerm_cases] >>
-      gs [] >>
-      last_x_assum (qspecl_then [‘st’, ‘m’, ‘i’, ‘st'’] mp_tac) >>
-      impl_tac
-      >- (
-        gs [] >>
-        gs [machine_bounds_def, tms_conds_eval_def, conds_eval_lt_dimword_def,
-            terms_time_range_def, input_terms_actions_def, terms_wtimes_ffi_bound_def,
-            terms_in_signals_def]) >>
-      strip_tac >>
-      gs [machine_bounds_def, terms_time_range_def,
-          conds_eval_lt_dimword_def, input_terms_actions_def,
-          terms_in_signals_def] >>
-      gs [tms_conds_eval_def, tm_conds_eval_def, EVERY_MEM] >>
-      rw [] >> gvs [timeLangTheory.termConditions_def] >>
-      res_tac >> gvs [] >>
-      FULL_CASE_TAC >> gvs []) >>
-    rewrite_tac [Once pickTerm_cases] >>
-    gs [] >>
-    last_x_assum (qspecl_then [‘st’, ‘m’, ‘i’, ‘st'’] mp_tac) >>
-    impl_tac
-    >- (
-      gs [] >>
-      gs [machine_bounds_def, tms_conds_eval_def, conds_eval_lt_dimword_def,
-          terms_time_range_def, input_terms_actions_def, terms_wtimes_ffi_bound_def,
-          terms_in_signals_def]) >>
-    strip_tac >>
-    gs [machine_bounds_def, terms_time_range_def,
-        conds_eval_lt_dimword_def, input_terms_actions_def,
-        terms_in_signals_def, tms_conds_eval_def,  tm_conds_eval_def,
-        timeLangTheory.termConditions_def] >>
-    gs [EVERY_MEM]) >>
-  rewrite_tac [Once pickTerm_cases] >>
-  gs [] >>
-  last_x_assum (qspecl_then [‘st’, ‘m’, ‘i’, ‘st'’] mp_tac) >>
-  impl_tac
-  >- (
-    gs [] >>
-    gs [machine_bounds_def, tms_conds_eval_def, conds_eval_lt_dimword_def,
-        terms_time_range_def, input_terms_actions_def, terms_wtimes_ffi_bound_def,
-        terms_in_signals_def]) >>
-  strip_tac >>
-  gs [machine_bounds_def, terms_time_range_def,
-      conds_eval_lt_dimword_def, input_terms_actions_def,
-      terms_in_signals_def]
-QED
-
-Theorem pick_eval_output_term_panic_imp_pickTerm:
-  ∀tms st m st'.
-    machine_bounds (resetOutput st) m tms ∧
-    pick_eval_output_term (resetOutput st) tms =
-    SOME (LPanic PanicTimeout, st') ⇒
-    pickTerm (resetOutput st) m NONE tms st' (LPanic PanicTimeout)
-Proof
-  Induct >>
-  rpt gen_tac >>
-  strip_tac >>
-  gs []
-  >- (
-    gs [pick_eval_output_term_def] >>
-    rewrite_tac [Once pickTerm_cases] >>
-    gs [machine_bounds_def]) >>
-  gs [pick_eval_output_term_def] >>
-  cases_on ‘h’ >> gs [] >>
-  reverse (cases_on ‘i’) >> gs []
-  >- (
-    FULL_CASE_TAC >> gs [] >> rveq >> gs []
-    >- (
-      rewrite_tac [Once pickTerm_cases] >>
-      gs [] >>
-      gs [machine_bounds_def, terms_time_range_def,
-          conds_eval_lt_dimword_def, input_terms_actions_def,
-          terms_in_signals_def] >>
-      gs [eval_term_def, evalTerm_cases] >>
-      rveq >> gs [state_component_equality]) >>
-    rewrite_tac [Once pickTerm_cases] >>
-    gs [] >>
-    last_x_assum (qspecl_then [‘st’, ‘m’, ‘st'’] mp_tac) >>
-    impl_tac
-    >- (
-      gs [] >>
-      gs [machine_bounds_def, tms_conds_eval_def, conds_eval_lt_dimword_def,
-          terms_time_range_def, input_terms_actions_def, terms_wtimes_ffi_bound_def,
-          terms_in_signals_def]) >>
-    strip_tac >>
-    gs [machine_bounds_def, terms_time_range_def,
-        conds_eval_lt_dimword_def, input_terms_actions_def,
-        terms_in_signals_def, tms_conds_eval_def,  tm_conds_eval_def,
-        timeLangTheory.termConditions_def] >>
-    gs [EVERY_MEM] >>
-    rw [] >>
-    res_tac >> gs []  >>
-    FULL_CASE_TAC >> gs []) >>
-  rewrite_tac [Once pickTerm_cases] >>
-  gs [] >>
-  last_x_assum (qspecl_then [‘st’, ‘m’, ‘st'’] mp_tac) >>
-  impl_tac
-  >- (
-    gs [] >>
-    gs [machine_bounds_def, tms_conds_eval_def, conds_eval_lt_dimword_def,
-        terms_time_range_def, input_terms_actions_def, terms_wtimes_ffi_bound_def,
-        terms_in_signals_def]) >>
-  strip_tac >>
-  gs [machine_bounds_def, terms_time_range_def,
-      conds_eval_lt_dimword_def, input_terms_actions_def,
-      terms_in_signals_def, tms_conds_eval_def,  tm_conds_eval_def,
-      timeLangTheory.termConditions_def]
-QED
-
-
-Theorem eval_step_imp_step:
-  eval_step prog m n or st = SOME (label, st') ⇒
-  step prog label m n st st'
-Proof
-  rw [] >>
-  fs [eval_step_def] >>
-  cases_on ‘st.waitTime’ >> gs [] >>
-  cases_on ‘or’ >> gs []
-  >- (
-    gs [eval_delay_wtime_none_def] >>
-    rveq >>
-    gs [step_cases, mkState_def] >>
-    gs [state_component_equality])
-  >- (
-    gs [eval_input_def] >>
-    FULL_CASE_TAC >> gvs [] >>
-    qmatch_asmsub_rename_tac ‘ALOOKUP _ _ = SOME tms’ >>
-    qmatch_asmsub_rename_tac ‘pick_eval_input_term _ i _ _ = _’ >>
-    drule label_from_pick_eval_input_term >>
-    strip_tac >> gvs []
-    >- (
-      imp_res_tac pick_eval_input_term_imp_pickTerm >>
-      gs [step_cases, mkState_def]) >>
-    drule_all pick_eval_input_term_panic_imp_pickTerm >>
-    gs [step_cases, mkState_def])
-  >- (
-    FULL_CASE_TAC >> gs []
-    >- (
-      gs [eval_output_def] >>
-      every_case_tac >> rveq >> gs [] >>
-      rveq >> gs [] >>
-      qmatch_asmsub_rename_tac ‘ALOOKUP _ _ = SOME tms’ >>
-      drule label_from_pick_eval_output_term >>
-      strip_tac >> gvs []
-      >- (
-        imp_res_tac pick_eval_output_term_imp_pickTerm >>
-        gs [step_cases, mkState_def]) >>
-      drule_all pick_eval_output_term_panic_imp_pickTerm >>
-      gs [step_cases, mkState_def]) >>
-    gs [eval_delay_wtime_some_def] >>
-    rveq >>
-    gs [step_cases, mkState_def] >>
-    gs [state_component_equality]) >>
-  cases_on ‘x = 0’ >> gs []
-  >- (
-    gs [eval_output_def] >>
-    every_case_tac >> rveq >> gs [] >>
-    rveq >> gs [] >>
-    qmatch_asmsub_rename_tac ‘ALOOKUP _ _ = SOME tms’ >>
-    drule label_from_pick_eval_output_term >>
-    strip_tac >> gvs []
-    >- (
-      imp_res_tac pick_eval_output_term_imp_pickTerm >>
-      gs [step_cases, mkState_def]) >>
-    drule_all pick_eval_output_term_panic_imp_pickTerm >>
-    gs [step_cases, mkState_def]) >>
-  gs [eval_input_def] >>
-  FULL_CASE_TAC >> gs [] >> rveq >> gs [] >>
-  qmatch_asmsub_rename_tac ‘ALOOKUP _ _ = SOME tms’ >>
-  qmatch_asmsub_rename_tac ‘pick_eval_input_term _ i _ _ = _’ >>
-  drule label_from_pick_eval_input_term >>
-  strip_tac >> gvs []
-  >- (
-    imp_res_tac pick_eval_input_term_imp_pickTerm >>
-    gs [step_cases, mkState_def]) >>
-  drule_all pick_eval_input_term_panic_imp_pickTerm >>
-  gs [step_cases, mkState_def]
-QED
-
-
-Theorem eval_steps_imp_steps:
-  ∀k prog m n or st labels sts.
-    eval_steps k prog m n or st = SOME (labels, sts) ⇒
-    steps prog labels m n st sts
-Proof
-  Induct >> rw []
-  >- fs [eval_steps_def, steps_def] >>
-  gs [eval_steps_def] >>
-  every_case_tac >> gvs [] >>
-  TRY (cases_on ‘p’) >> gvs [] >>
-  gs [steps_def] >>
-  imp_res_tac eval_step_imp_step >>
-  gs [] >>
-  res_tac >> gs []
-QED
-
-val _ = export_theory();
diff --git a/pancake/semantics/timePropsScript.sml b/pancake/semantics/timePropsScript.sml
deleted file mode 100644
index c0ee880b33..0000000000
--- a/pancake/semantics/timePropsScript.sml
+++ /dev/null
@@ -1,257 +0,0 @@
-(*
-  semantics for timeLang
-*)
-
-open preamble
-     timeLangTheory timeSemTheory
-     pan_commonPropsTheory
-
-val _ = new_theory "timeProps";
-
-val _ = set_grammar_ancestry
-        ["timeLang","timeSem",
-         "pan_commonProps"];
-
-Theorem eval_term_inpput_ios_same:
-  ∀s m n cnds tclks dest wt s'.
-    evalTerm s (SOME m) (Tm (Input n) cnds tclks dest wt) s' ⇒
-    m = n
-Proof
-  rw [] >>
-  fs [evalTerm_cases]
-QED
-
-
-Theorem eval_term_clocks_reset:
-  ∀s io n cnds tclks dest wt s' ck t.
-    FLOOKUP s.clocks ck = SOME t ∧
-    evalTerm s io (Tm n cnds tclks dest wt) s' ⇒
-    (FLOOKUP s'.clocks ck = SOME t ∨ FLOOKUP s'.clocks ck = SOME 0)
-Proof
-  rw [] >>
-  fs [evalTerm_cases, resetClocks_def] >>
-  rveq >> gs [] >>(
-  cases_on ‘MEM ck tclks’
-  >- (
-    gs [MEM_EL] >>
-    metis_tac [update_eq_zip_map_flookup]) >>
-  last_x_assum (assume_tac o GSYM) >>
-  gs [] >>
-  disj1_tac >>
-  match_mp_tac flookup_fupdate_zip_not_mem >>
-  gs [])
-QED
-
-
-Theorem list_min_option_some_mem:
-  ∀xs x.
-    list_min_option xs = SOME x ⇒
-    MEM x xs
-Proof
-  Induct >> rw [] >>
-  fs [list_min_option_def] >>
-  every_case_tac >> fs [] >> rveq >> rfs []
-QED
-
-
-Theorem fdom_reset_clks_eq_clks:
-  ∀fm clks.
-    EVERY (λck. ck IN FDOM fm) clks ⇒
-    FDOM (resetClocks fm clks) = FDOM fm
-Proof
-  rw [] >>
-  fs [resetClocks_def] >>
-  fs [FDOM_FUPDATE_LIST] >>
-  ‘LENGTH clks = LENGTH (MAP (λx. 0:num) clks)’ by fs [] >>
-  drule MAP_ZIP >>
-  fs [] >>
-  strip_tac >> pop_assum kall_tac >>
-  ‘set clks ⊆ FDOM fm’ by (
-    fs [SUBSET_DEF] >>
-    rw [] >>
-    fs [EVERY_MEM]) >>
-  fs [SUBSET_UNION_ABSORPTION] >>
-  fs [UNION_COMM]
-QED
-
-
-Theorem reset_clks_mem_flookup_zero:
-  ∀clks ck fm.
-    MEM ck clks ⇒
-    FLOOKUP (resetClocks fm clks) ck = SOME 0
-Proof
-  rw [] >>
-  fs [timeSemTheory.resetClocks_def] >>
-  fs [MEM_EL] >> rveq >>
-  match_mp_tac update_eq_zip_map_flookup >> fs []
-QED
-
-
-
-Theorem reset_clks_not_mem_flookup_same:
-  ∀clks ck fm v.
-    FLOOKUP fm ck = SOME v ∧
-    ~MEM ck clks ⇒
-    FLOOKUP (resetClocks fm clks) ck = SOME v
-Proof
-  rw [] >>
-  fs [timeSemTheory.resetClocks_def] >>
-  last_x_assum (mp_tac o GSYM) >>
-  fs [] >>
-  strip_tac >>
-  match_mp_tac flookup_fupdate_zip_not_mem >>
-  fs []
-QED
-
-
-Theorem flookup_reset_clks_leq:
-  ∀fm ck v tclks q.
-    FLOOKUP fm ck = SOME v ∧ v ≤ q ⇒
-    ∃v. FLOOKUP (resetClocks fm tclks) ck = SOME v ∧ v ≤ q
-Proof
-  rw [] >>
-  cases_on ‘MEM ck tclks’
-  >- (
-    drule reset_clks_mem_flookup_zero >>
-    fs []) >>
-  drule reset_clks_not_mem_flookup_same >>
-  fs []
-QED
-
-
-Theorem exprClks_accumulates:
-  ∀xs e ys.
-    EVERY (λck. MEM ck ys) (exprClks xs e) ⇒
-    EVERY (λck. MEM ck ys) xs
-Proof
-  ho_match_mp_tac exprClks_ind >>
-  rw [] >>
-  cases_on ‘e’
-  >- fs [Once exprClks_def]
-  >- (
-   gs [] >>
-   fs [exprClks_def] >>
-   every_case_tac >> fs []) >>
-  gs [] >>
-  pop_assum mp_tac >>
-  once_rewrite_tac [exprClks_def] >>
-  fs []
-QED
-
-
-Theorem exprClks_sublist_accum:
-  ∀xs e ck ys.
-    MEM ck (exprClks xs e) ∧
-    EVERY (λx. MEM x ys) xs ⇒
-    MEM ck (exprClks ys e)
-Proof
-  ho_match_mp_tac exprClks_ind >>
-  rw [] >>
-  gs [] >>
-  cases_on ‘e’
-  >- fs [Once exprClks_def, EVERY_MEM]
-  >- (
-    gs [] >>
-    fs [exprClks_def] >>
-    every_case_tac >> gs [EVERY_MEM]) >>
-  gs [] >>
-  once_rewrite_tac [exprClks_def] >>
-  fs [] >>
-  first_x_assum match_mp_tac >>
-  conj_tac
-  >- (
-    qpat_x_assum ‘MEM ck _’ mp_tac >>
-    rewrite_tac [Once exprClks_def] >>
-    fs []) >>
-  fs [EVERY_MEM]
-QED
-
-
-Theorem terms_out_signals_append:
-  ∀xs ys.
-    terms_out_signals (xs ++ ys) =
-    terms_out_signals xs ++ terms_out_signals ys
-Proof
-  Induct >> rw [] >>
-  gs [timeLangTheory.terms_out_signals_def] >>
-  cases_on ‘h’ >> gs [] >>
-  cases_on ‘i’ >> gs [timeLangTheory.terms_out_signals_def]
-QED
-
-
-Theorem terms_out_signals_prog:
-  ∀xs x out.
-    MEM x xs ∧
-    MEM out (terms_out_signals x) ⇒
-    MEM out (terms_out_signals (FLAT xs))
-Proof
-  Induct >> rw [] >>
-  gs [timeLangTheory.terms_out_signals_def] >>
-  gs [terms_out_signals_append] >>
-  metis_tac []
-QED
-
-Theorem calculate_wtime_reset_output_eq:
-  calculate_wtime s clks difs = SOME wt ⇒
-  calculate_wtime (resetOutput s) clks difs = SOME wt
-Proof
-  rw [calculate_wtime_def, resetOutput_def] >>
-  gs [] >>
-  qmatch_asmsub_abbrev_tac ‘list_min_option xs’ >>
-  qmatch_goalsub_abbrev_tac ‘list_min_option ys’ >>
-  ‘xs = ys’ by (
-    unabbrev_all_tac >>
-    gs [MAP_EQ_f] >>
-    rw [] >> gs [] >>
-    cases_on ‘e’ >>
-    gs [evalDiff_def, evalExpr_def]) >>
-  gs []
-QED
-
-
-Theorem step_ffi_bounded:
-  ∀p lbl m n st st'.
-    step p lbl m n st st' ⇒
-    n < m
-Proof
-  rw [] >>
-  gs [step_cases]
-QED
-
-Theorem steps_ffi_bounded:
-  ∀lbls sts p m n st.
-    steps p lbls m n st sts ∧
-    lbls ≠ [] ⇒
-    n < m
-Proof
-  Induct >>
-  rw [] >>
-  cases_on ‘sts’ >>
-  gs [steps_def, step_cases]
-QED
-
-Theorem steps_lbls_sts_len_eq:
-  ∀lbls sts p m n st.
-    steps p lbls m n st sts ⇒
-    LENGTH lbls = LENGTH sts
-Proof
-  Induct >>
-  rw [] >>
-  cases_on ‘sts’ >>
-  gs [steps_def, step_cases] >>
-  res_tac >> gs []
-QED
-
-Theorem pickTerm_panic_st_eq:
-  ∀tms st m i st st'.
-    pickTerm st m (SOME i) tms st' (LPanic (PanicInput i)) ⇒
-    st' = st
-Proof
- Induct >> rw [] >>
- rgs [Once pickTerm_cases] >>
- gvs [] >>
- res_tac >> gs []
-QED
-
-
-val _ = export_theory();
diff --git a/pancake/semantics/timeSemScript.sml b/pancake/semantics/timeSemScript.sml
deleted file mode 100644
index 55fe981746..0000000000
--- a/pancake/semantics/timeSemScript.sml
+++ /dev/null
@@ -1,390 +0,0 @@
-(*
-  semantics for timeLang
-*)
-
-open preamble
-     timeLangTheory
-
-val _ = new_theory "timeSem";
-
-Datatype:
-  panic = PanicTimeout
-        | PanicInput in_signal
-End
-
-Datatype:
-  label = LDelay time
-        | LAction ioAction
-        | LPanic panic
-End
-
-Datatype:
-  state =
-  <| clocks   : clock |-> time
-   ; location : loc
-   ; ioAction : ioAction option
-   ; waitTime : time option
-  |>
-End
-
-
-Definition mkState_def:
-  mkState cks loc io wt =
-  <| clocks   := cks
-   ; location := loc
-   ; ioAction := io
-   ; waitTime := wt
-  |>
-End
-
-Definition resetOutput_def:
-  resetOutput st =
-  st with
-  <| ioAction := NONE
-   ; waitTime := NONE
-  |>
-End
-
-Definition resetClocks_def:
-  resetClocks fm xs =
-    fm |++ ZIP (xs,MAP (λx. 0:time) xs)
-End
-
-(* TODO: rephrase this def *)
-
-Definition list_min_option_def:
-  (list_min_option ([]:num list) = NONE) /\
-  (list_min_option (x::xs) =
-   case list_min_option xs of
-   | NONE => SOME x
-   | SOME y => SOME (if x < y then x else y))
-End
-
-Definition delay_clocks_def:
-  delay_clocks fm (d:num) = FEMPTY |++
-                            (MAP (λ(x,y). (x,y+d))
-                            (fmap_to_alist fm))
-End
-
-
-Definition minusT_def:
-  minusT (t1:time) (t2:time) = t1 - t2
-End
-
-(* inner case for generating induction theorem *)
-
-Definition evalExpr_def:
-  evalExpr st e =
-  case e of
-  | ELit t => SOME t
-  | EClock c => FLOOKUP st.clocks c
-  | ESub e1 e2 =>
-      case (evalExpr st e1, evalExpr st e2) of
-      | SOME t1,SOME t2 =>
-                  if t2 ≤ t1 then SOME (minusT t1 t2)
-                  else NONE
-      | _=> NONE
-End
-
-
-Definition evalCond_def:
-  (evalCond st (CndLe e1 e2) =
-    case (evalExpr st e1,evalExpr st e2) of
-    | SOME t1,SOME t2 => t1 ≤ t2
-    | _ => F) ∧
-  (evalCond st (CndLt e1 e2) =
-    case (evalExpr st e1,evalExpr st e2) of
-    | SOME t1,SOME t2 => t1 < t2
-    | _ => F)
-End
-
-
-Definition evalDiff_def:
-  evalDiff st ((t,c): time # clock) =
-    evalExpr st (ESub (ELit t) (EClock c))
-End
-
-
-Definition calculate_wtime_def:
-  calculate_wtime st clks diffs =
-  let
-    st = st with clocks := resetClocks st.clocks clks
-  in
-    list_min_option (MAP (THE o evalDiff st) diffs)
-End
-
-
-Inductive evalTerm:
-  (∀st in_signal cnds clks dest diffs.
-     EVERY (λck. ck IN FDOM st.clocks) clks ∧
-     EVERY (λ(t,c).
-             ∃v. FLOOKUP st.clocks c = SOME v ∧
-                 v ≤ t) diffs ==>
-     evalTerm st (SOME in_signal)
-              (Tm (Input in_signal)
-                  cnds
-                  clks
-                  dest
-                  diffs)
-              (st with  <| clocks   := resetClocks st.clocks clks
-                         ; ioAction := SOME (Input in_signal)
-                         ; location := dest
-                         ; waitTime := calculate_wtime st clks diffs|>)) /\
-  (∀st out_signal cnds clks dest diffs.
-     EVERY (λck. ck IN FDOM st.clocks) clks ∧
-     EVERY (λ(t,c).
-             ∃v. FLOOKUP st.clocks c = SOME v ∧
-                 v ≤ t) diffs ==>
-     evalTerm st NONE
-              (Tm (Output out_signal)
-                  cnds
-                  clks
-                  dest
-                  diffs)
-              (st with  <| clocks   := resetClocks st.clocks clks
-                         ; ioAction := SOME (Output out_signal)
-                         ; location := dest
-                         ; waitTime := calculate_wtime st clks diffs|>))
-End
-
-Definition max_clocks_def:
-  max_clocks fm (m:num) ⇔
-  ∀ck n.
-    FLOOKUP fm ck = SOME n ⇒
-    n < m
-End
-
-
-Definition tm_conds_eval_def:
-  tm_conds_eval s tm =
-    EVERY (λcnd.
-            EVERY (λe. case (evalExpr s e) of
-                       | SOME n => T
-                       | _ => F) (destCond cnd))
-          (termConditions tm)
-End
-
-
-Definition tms_conds_eval_def:
-  tms_conds_eval s tms =
-    EVERY (tm_conds_eval s) tms
-End
-
-Definition tm_conds_eval_limit_def:
-  tm_conds_eval_limit m s tm =
-    EVERY (λcnd.
-            EVERY (λe. case (evalExpr s e) of
-                       | SOME n => n < m
-                       | _ => F) (destCond cnd))
-          (termConditions tm)
-End
-
-
-Definition conds_eval_lt_dimword_def:
-  conds_eval_lt_dimword m s tms =
-    EVERY (tm_conds_eval_limit m s) tms
-End
-
-
-Definition time_range_def:
-  time_range wt (m:num) ⇔
-    EVERY (λ(t,c). t < m) wt
-End
-
-
-Definition term_time_range_def:
-  term_time_range m tm =
-    time_range (termWaitTimes tm) m
-End
-
-Definition terms_time_range_def:
-  terms_time_range m tms =
-    EVERY (term_time_range m) tms
-End
-
-Definition input_terms_actions_def:
-  input_terms_actions m tms =
-    EVERY (λn. n+1 < m)
-          (terms_in_signals tms)
-End
-
-Definition terms_wtimes_ffi_bound_def:
-  terms_wtimes_ffi_bound m s tms =
-    EVERY (λtm.
-            case calculate_wtime (resetOutput s) (termClks tm) (termWaitTimes tm) of
-            | NONE => T
-            | SOME wt => wt < m
-          ) tms
-End
-
-(* max is dimword *)
-(* m is m+n *)
-Inductive pickTerm:
-  (!st m cnds in_signal clks dest diffs tms st'.
-    EVERY (λcnd. evalCond st cnd) cnds ∧
-    conds_eval_lt_dimword m st (Tm (Input in_signal) cnds clks dest diffs::tms) ∧
-    max_clocks st.clocks m ∧
-    terms_time_range m (Tm (Input in_signal) cnds clks dest diffs::tms)  ∧
-    input_terms_actions m (Tm (Input in_signal) cnds clks dest diffs::tms) ∧
-    terms_wtimes_ffi_bound m st (Tm (Input in_signal) cnds clks dest diffs::tms) ∧
-    evalTerm st (SOME in_signal) (Tm (Input in_signal) cnds clks dest diffs) st' ⇒
-    pickTerm st m (SOME in_signal) (Tm (Input in_signal) cnds clks dest diffs::tms) st'
-             (LAction (Input in_signal))) ∧
-
-  (!st m cnds out_signal clks dest diffs tms st'.
-    EVERY (λcnd. evalCond st cnd) cnds ∧
-    conds_eval_lt_dimword m st (Tm (Output out_signal) cnds clks dest diffs::tms) ∧
-    max_clocks st.clocks m ∧
-    terms_time_range m (Tm (Output out_signal) cnds clks dest diffs::tms) ∧
-    input_terms_actions m tms ∧
-    terms_wtimes_ffi_bound m st (Tm (Output out_signal) cnds clks dest diffs::tms) ∧
-    evalTerm st NONE (Tm (Output out_signal) cnds clks dest diffs) st' ⇒
-    pickTerm st m NONE (Tm (Output out_signal) cnds clks dest diffs::tms) st'
-             (LAction (Output out_signal))) ∧
-
-  (!st m cnds event ioAction clks dest diffs tms st' lbl.
-    EVERY (λcnd. EVERY (λe. ∃t. evalExpr st e = SOME t) (destCond cnd)) cnds ∧
-    ~(EVERY (λcnd. evalCond st cnd) cnds) ∧
-    tm_conds_eval_limit m st (Tm ioAction cnds clks dest diffs) ∧
-    term_time_range m (Tm ioAction cnds clks dest diffs) ∧
-    input_terms_actions m [(Tm ioAction cnds clks dest diffs)] ∧
-    terms_wtimes_ffi_bound m st (Tm ioAction cnds clks dest diffs :: tms) ∧
-    pickTerm st m event tms st' lbl ⇒
-    pickTerm st m event (Tm ioAction cnds clks dest diffs :: tms) st' lbl) ∧
-
-  (!st m cnds event in_signal clks dest diffs tms st' lbl.
-    event <> SOME in_signal ∧
-    tm_conds_eval_limit m st (Tm (Input in_signal) cnds clks dest diffs) ∧
-    term_time_range m (Tm (Input in_signal) cnds clks dest diffs) ∧
-    terms_wtimes_ffi_bound m st (Tm (Input in_signal) cnds clks dest diffs :: tms) ∧
-    in_signal + 1 < m ∧
-    pickTerm st m event tms st' lbl ⇒
-    pickTerm st m event (Tm (Input in_signal) cnds clks dest diffs :: tms) st' lbl) ∧
-
-  (!st m cnds event out_signal clks dest diffs tms st' lbl.
-    event <> NONE ∧
-    tm_conds_eval_limit m st (Tm (Output out_signal) cnds clks dest diffs) ∧
-    term_time_range m (Tm (Output out_signal) cnds clks dest diffs) ∧
-    terms_wtimes_ffi_bound m st (Tm (Output out_signal) cnds clks dest diffs :: tms) ∧
-    pickTerm st m event tms st' lbl ⇒
-    pickTerm st m event (Tm (Output out_signal) cnds clks dest diffs :: tms) st' lbl) ∧
-
-  (!st m.
-    max_clocks st.clocks m  ⇒
-    pickTerm st m NONE [] st (LPanic PanicTimeout)) ∧
-
-  (!st m in_signal.
-    max_clocks st.clocks m ∧
-    in_signal + 1 < m ⇒
-    pickTerm st m (SOME in_signal) [] st (LPanic (PanicInput in_signal)))
-End
-
-(* d + n ≤ m ∧ *)
-
-(* m ≤ w + n *)
-(* n would be FST (seq 0), or may be systime time *)
-Inductive step:
-  (!p m n st d.
-    st.waitTime = NONE ∧
-    d + n < m ∧
-    max_clocks (delay_clocks (st.clocks) (d + n)) m ⇒
-    step p (LDelay d) m n st
-         (mkState
-          (delay_clocks (st.clocks) d)
-          st.location
-          NONE
-          NONE)) ∧
-
-  (!p m n st d w.
-    st.waitTime = SOME w ∧
-    d ≤ w ∧ w < m ∧ d + n < m ∧
-    max_clocks (delay_clocks (st.clocks) (d + n)) m ⇒
-    step p (LDelay d) m n st
-         (mkState
-          (delay_clocks (st.clocks) d)
-          st.location
-          NONE
-          (SOME (w - d)))) ∧
-
-  (!p m n st tms st' in_signal.
-    n < m ∧
-    ALOOKUP p st.location = SOME tms ∧
-    (case st.waitTime of
-     | NONE => T
-     | SOME wt => wt ≠ 0 ∧ wt < m) ∧
-    pickTerm (resetOutput st) m (SOME in_signal) tms st' (LAction (Input in_signal)) ∧
-    st'.ioAction = SOME (Input in_signal) ⇒
-    step p (LAction (Input in_signal)) m n st st') ∧
-
-  (!p m n st tms st' out_signal.
-    n < m ∧
-    ALOOKUP p st.location = SOME tms ∧
-    st.waitTime = SOME 0 ∧
-    pickTerm (resetOutput st) m NONE tms st' (LAction (Output out_signal)) ∧
-    st'.ioAction = SOME (Output out_signal) ⇒
-    step p (LAction (Output out_signal)) m n st st') ∧
-
-  (!p m n st tms st'.
-    n < m ∧
-    ALOOKUP p st.location = SOME tms ∧
-    st.waitTime = SOME 0 ∧
-    pickTerm (resetOutput st) m NONE tms st' (LPanic PanicTimeout) ⇒
-    step p (LPanic PanicTimeout) m n st st') ∧
-
-  (!p m n st tms st' in_signal.
-    n < m ∧
-    ALOOKUP p st.location = SOME tms ∧
-    (case st.waitTime of
-     | NONE => T
-     | SOME wt => wt ≠ 0 ∧ wt < m) ∧
-    pickTerm (resetOutput st) m (SOME in_signal) tms st' (LPanic (PanicInput in_signal)) ⇒
-    step p (LPanic (PanicInput in_signal)) m n st st')
-End
-
-
-Definition steps_def:
-  (steps prog [] m n s [] ⇔ T) ∧
-  (steps prog (lbl::lbls) m n s (st::sts) ⇔
-     step prog lbl m n s st ∧
-     let n' =
-         case lbl of
-         | LDelay d => d + n
-         | _ => n
-     in
-       steps prog lbls m n' st sts) ∧
-  (steps prog _ m _ s _ ⇔ F)
-End
-
-(*
-Definition steps_def:
-  (steps prog [] m n s [] ⇔
-   n < m  ∧
-   (case s.waitTime of
-    | SOME w => (* w ≠ 0 ∧ *) w < m
-    | NONE => T)) ∧
-  (steps prog (lbl::lbls) m n s (st::sts) ⇔
-     step prog lbl m n s st ∧
-     let n' =
-         case lbl of
-         | LDelay d => d + n
-         | _ => n
-     in
-       steps prog lbls m n' st sts) ∧
-  (steps prog _ m _ s _ ⇔ F)
-End
-*)
-Inductive stepTrace:
-  (!p m n st.
-    stepTrace p m n st st []) ∧
-
-  (!p lbl m n st st' st'' tr.
-    step p lbl m n st st' ∧
-    stepTrace p m (case lbl of
-                   | LDelay d => d + n
-                   | LAction _ => n)
-              st' st'' tr ⇒
-    stepTrace p m n st st'' (lbl::tr))
-End
-
-
-val _ = export_theory();
diff --git a/pancake/sketch.txt b/pancake/sketch.txt
deleted file mode 100644
index d3ae3f550c..0000000000
--- a/pancake/sketch.txt
+++ /dev/null
@@ -1,53 +0,0 @@
-REPRESENTATION:
-
-  state s          state t
-
-                   the global system clock as 'a word
-
-  store_clocks --> global vars in Pancake, each as 'a word
-
-  wait NONE    --> as 0w in wait_set var   -- never wake me up (unless there is an input)
-  wait SOME c  --> wait_set is 1w          -- some wake up time is present
-               --> wake_up_at is c as 'a word
-
-  location     --> Lab funname   (where the code for location is implemented in funname)
-
-
-state_rel:
-
-     s.clocks A = t.sys_time - t.locals "A_time"
-
-     IS_SOME (s.wait) <=> t.locals "wait_set" = 1w
-
-     s.wait = SOME c ==>
-       c = t.locals "wake_up_at" - t.sys_time
-
-
-IMPLEMENTATION:
-
-  sketch:
-
-    input_received = false;
-    input = null;
-    sys_time = get_time_now();
-    while ((wait_set ==> sys_time < wake_up_at) && !input_received) {
-      input_received = check_for_input(); // updates input is received
-      sys_time = get_time_now();
-    }
-    Call (Ret (Var "location") NONE) (Var "location") [Var "sys_time"]
-
-
-timeLang:
-  Type program = (location # (term list)) list
-
-  timeLang program turns into the list of Pancake functions
-
-     one should think:  location -> term list
-
-     compile ([]:term list) = Skip /\
-     compile (x::xs) = compile_single x (compile xs)
-
-     compiler_single (Term io cond next_loc clocks_to_reset wait) otherwise =
-       panLang$If (compile_cond cond)
-                 (compile_body io next_loc clocks_to_reset wait)
-                 otherwise
diff --git a/pancake/taParserScript.sml b/pancake/taParserScript.sml
deleted file mode 100644
index 3f059314b3..0000000000
--- a/pancake/taParserScript.sml
+++ /dev/null
@@ -1,49 +0,0 @@
-(*
-  Parser for compactDSL programs
-*)
-
-open preamble
-     timeLangTheory
-
-val _ = new_theory "taParser";
-
-Overload CVar = “strlit”;
-
-local
-  fun has_nat_prefix (#"%" :: #"n" :: #"a" :: #"t" :: _) = true
-    | has_nat_prefix _ = false
-
-  fun replace_nat_chars [] = []
-    | replace_nat_chars xs =
-        if has_nat_prefix xs
-        then #"n" :: replace_nat_chars (List.drop(xs,4))
-        else hd xs :: replace_nat_chars (tl xs)
-
-  val replace_nat = implode o replace_nat_chars o explode
-in
-  fun parseFile fname filename =
-    let
-        val fd = TextIO.openIn filename
-        val content = TextIO.inputAll fd handle e => (TextIO.closeIn fd; raise e)
-        val _ = TextIO.closeIn fd
-        val content = replace_nat content
-    in
-      Define [QUOTE (fname ^ " " ^ content)]
-    end
-end
-
-Overload CVar = “strlit”
-
-val flashing_led_def =
-      parseFile "flashing_led"
-                "ta_progs/flashing_led.out";
-
-val flashing_led_with_button_def =
-      parseFile "flashing_led_with_button"
-                "ta_progs/flashing_led_with_button.out";
-
-val flashing_led_with_invariant_def =
-      parseFile "flashing_led_with_invariant"
-                "ta_progs/flashing_led_with_invariant.out";
-
-val _ = export_theory();
diff --git a/pancake/ta_progs/Holmakefile b/pancake/ta_progs/Holmakefile
deleted file mode 100644
index 658ab94ad5..0000000000
--- a/pancake/ta_progs/Holmakefile
+++ /dev/null
@@ -1,7 +0,0 @@
-all: $(DEFAULT_TARGETS) README.md
-.PHONY: all
-
-README_SOURCES = $(wildcard *Script.sml) $(wildcard *Lib.sml) $(wildcard *Syntax.sml)
-DIRS = $(wildcard */)
-README.md: $(CAKEMLDIR)/developers/readme_gen readmePrefix $(patsubst %,%readmePrefix,$(DIRS)) $(README_SOURCES)
-	$(protect $(CAKEMLDIR)/developers/readme_gen) $(README_SOURCES)
diff --git a/pancake/ta_progs/README.md b/pancake/ta_progs/README.md
deleted file mode 100644
index 4936012e98..0000000000
--- a/pancake/ta_progs/README.md
+++ /dev/null
@@ -1 +0,0 @@
-Some sample timed automata (TA) programs.
diff --git a/pancake/ta_progs/flashing_led.out b/pancake/ta_progs/flashing_led.out
deleted file mode 100644
index b46f489bd1..0000000000
--- a/pancake/ta_progs/flashing_led.out
+++ /dev/null
@@ -1,13 +0,0 @@
-     = ([(0%nat,
-        [Tm (Output 1%nat)
-           [CndLe (EClock (CVar "x")) (ELit 1);
-           CndLe (ELit 1) (EClock (CVar "x"));
-           CndLe (EClock (CVar "x")) (ELit 2)] [] 1%nat
-	   [(2, CVar "x")]]);
-       (1%nat,
-       [Tm (Output 0%nat)
-          [CndLe (EClock (CVar "x")) (ELit 2);
-          CndLe (ELit 2) (EClock (CVar "x"));
-	  CndLe (ELit 0) (ELit 1)]
-          [CVar "x"] 0%nat [(1, CVar "x")]])], NONE)
-     : program
diff --git a/pancake/ta_progs/flashing_led_with_button.out b/pancake/ta_progs/flashing_led_with_button.out
deleted file mode 100644
index 1f82fa1552..0000000000
--- a/pancake/ta_progs/flashing_led_with_button.out
+++ /dev/null
@@ -1,23 +0,0 @@
-     = ([(0%nat,
-        [Tm (Output 1%nat)
-           [CndLe (EClock (CVar "x")) (ELit 1);
-           CndLe (ELit 1) (EClock (CVar "x"));
-           CndLe (EClock (CVar "x")) (ELit 2)] [] 2%nat [(2, CVar "x")];
-        Tm (Input 0%nat) [] [] 1%nat []]);
-       (1%nat,
-       [Tm (Input 1%nat) [CndLe (ELit 0) (ELit 1)] [CVar "x"] 0%nat
-          [(1, CVar "x")]]);
-       (2%nat,
-       [Tm (Output 0%nat)
-          [CndLe (EClock (CVar "x")) (ELit 2);
-          CndLe (ELit 2) (EClock (CVar "x")); CndLe (ELit 0) (ELit 1)]
-          [CVar "x"] 0%nat [(1, CVar "x")];
-       Tm (Input 0%nat) [CndLe (EClock (CVar "x")) (ELit 2)] [] 3%nat
-         [(2, CVar "x")]]);
-       (3%nat,
-       [Tm (Input 1%nat) [CndLe (EClock (CVar "x")) (ELit 2)] [] 2%nat
-          [(2, CVar "x")];
-       Tm (Output 2%nat)
-         [CndLe (EClock (CVar "x")) (ELit 2);
-         CndLe (ELit 2) (EClock (CVar "x"))] [] 1%nat []])], SOME 10)
-     : program
diff --git a/pancake/ta_progs/flashing_led_with_invariant.out b/pancake/ta_progs/flashing_led_with_invariant.out
deleted file mode 100644
index cbf4d89772..0000000000
--- a/pancake/ta_progs/flashing_led_with_invariant.out
+++ /dev/null
@@ -1,25 +0,0 @@
-     = ([(0%nat,
-        [Tm (Output 1%nat)
-           [CndLe (EClock (CVar "x")) (ELit 1);
-           CndLe (ELit 1) (EClock (CVar "x"));
-           CndLe (EClock (CVar "x")) (ELit 2)] [] 2%nat [(2, CVar "x")];
-        Tm (Input 0%nat) [CndLt (ELit 0) (ELit 5)] [CVar "y"] 1%nat
-          [(5, CVar "y")]]);
-       (1%nat,
-       [Tm (Input 1%nat) [CndLe (ELit 0) (ELit 1)] [CVar "x"] 0%nat
-          [(1, CVar "x")]]);
-       (2%nat,
-       [Tm (Output 0%nat)
-          [CndLe (EClock (CVar "x")) (ELit 2);
-          CndLe (ELit 2) (EClock (CVar "x")); CndLe (ELit 0) (ELit 1)]
-          [CVar "x"] 0%nat [(1, CVar "x")];
-       Tm (Input 0%nat) [CndLe (EClock (CVar "x")) (ELit 2)] [CVar "y"] 3%nat
-         [(2, CVar "x")]]);
-       (3%nat,
-       [Tm (Input 1%nat) [CndLe (EClock (CVar "x")) (ELit 2)] [] 2%nat
-          [(2, CVar "x")];
-       Tm (Output 2%nat)
-         [CndLe (EClock (CVar "x")) (ELit 2);
-         CndLe (ELit 2) (EClock (CVar "x"));
-         CndLt (EClock (CVar "y")) (ELit 5)] [] 1%nat [(5, CVar "y")]])], SOME 1)
-     : program
diff --git a/pancake/ta_progs/readmePrefix b/pancake/ta_progs/readmePrefix
deleted file mode 100644
index 4936012e98..0000000000
--- a/pancake/ta_progs/readmePrefix
+++ /dev/null
@@ -1 +0,0 @@
-Some sample timed automata (TA) programs.
diff --git a/pancake/timeLangScript.sml b/pancake/timeLangScript.sml
deleted file mode 100644
index 5c8895ca83..0000000000
--- a/pancake/timeLangScript.sml
+++ /dev/null
@@ -1,189 +0,0 @@
-(*
-  Abstract syntax for timeLang
-*)
-
-open preamble
-     stringTheory mlstringTheory mlintTheory
-
-val _ = new_theory "timeLang";
-
-Overload CVar[inferior] = “strlit”
-
-val _ = set_grammar_ancestry
-        ["mlint"];
-
-(* location identifies TA-states *)
-Type loc = ``:num``
-
-(* state specific input and output *)
-Type in_signal  = ``:num``
-Type out_signal = ``:num``
-
-Datatype:
-  ioAction = Input  in_signal
-           | Output out_signal
-End
-
-(*
-  IMP:
-  time:rat in the Coq formalism,
-  Pancake has discrete time:num  *)
-Type time   = ``:num``
-
-(* clock variables *)
-Type clock  = ``:mlstring``
-Type clocks = ``:clock list``
-
-(* time expression *)
-Datatype:
-  expr = ELit time
-       | EClock clock
-       | ESub expr expr
-End
-
-(* relational time expression *)
-Datatype:
-  cond = CndLe expr expr  (* e <= e *)
-       | CndLt expr expr  (* e < e *)
-End
-
-Datatype:
-  term = Tm ioAction
-            (cond list)
-            clocks
-            loc
-            ((time # clock) list) (* to calculate wait time *)
-End
-
-(*
-Type program = ``:(loc # term list) list``
-*)
-
-Type program = ``:(loc # term list) list # time option``
-
-(* functions for compiler *)
-Definition termConditions_def:
-  (termConditions (Tm _ cs _ _ _) = cs)
-End
-
-Definition termWaitTimes_def:
-  (termWaitTimes (Tm _ _ _ _ wt) = wt)
-End
-
-Definition termDest_def:
-  (termDest (Tm _ _ _ loc _) = loc)
-End
-
-Definition termAction_def:
-  (termAction (Tm io _ _ _ _) = io)
-End
-
-
-Definition terms_out_signals_def:
-  (terms_out_signals [] = []) ∧
-  (terms_out_signals (Tm (Output out) _ _ _ _::tms) =
-   out :: terms_out_signals tms) ∧
-  (terms_out_signals (Tm (Input _) _ _ _ _::tms) =
-   terms_out_signals tms)
-End
-
-
-Definition terms_in_signals_def:
-  (terms_in_signals [] = []) ∧
-  (terms_in_signals (Tm (Input i) _ _ _ _::tms) =
-   i :: terms_in_signals tms) ∧
-  (terms_in_signals (Tm (Output _) _ _ _ _::tms) =
-   terms_in_signals tms)
-End
-
-Definition accumClks_def:
-  (accumClks ac [] = ac) ∧
-  (accumClks ac (clk::clks) =
-   if MEM clk ac
-   then accumClks ac clks
-   else accumClks (clk::ac) clks)
-End
-
-
-Definition exprClks_def:
-  exprClks clks e =
-  case e of
-  | ELit t => clks
-  | EClock clk =>
-     if MEM clk clks then clks else clk::clks
-  | ESub e1 e2 =>
-     exprClks (exprClks clks e1) e2
-End
-
-
-Definition clksOfExprs_def:
-  clksOfExprs es = FOLDL exprClks [] es
-End
-
-
-Definition destCond_def:
-  (destCond (CndLe e1 e2) = [e1; e2]) ∧
-  (destCond (CndLt e1 e2) = [e1; e2])
-End
-
-
-Definition condClks_def:
-  condClks cd = clksOfExprs (destCond cd)
-End
-
-
-Definition condsClks_def:
-  condsClks cds = clksOfExprs (FLAT (MAP destCond cds))
-End
-
-
-Definition termClks_def:
-  termClks (Tm _ _ clks _ _) = clks
-End
-
-
-Definition clksOf_def:
-  clksOf prog =
-  let tms = FLAT (MAP SND prog) in
-     accumClks [] (FLAT (MAP termClks tms))
-End
-
-Definition nClks_def:
-  nClks prog = LENGTH (clksOf prog)
-End
-
-
-Definition termInvs_def:
-  termInvs (Tm _ _ _ _ tes) = MAP FST tes
-End
-
-Definition initTerm_def:
-  (initTerm (t::ts) = t) ∧
-  (initTerm [] = [])
-End
-
-
-Definition initLoc_def:
-  initLoc = 0:num
-End
-
-Definition waitSet_def:
-  (waitSet (Tm _ _ _ _ []) = 0:num) ∧
-  (waitSet _ = 1:num)
-End
-
-Definition inputSet_def:
-  (inputSet (Tm _ _ _ _ []) = 1:num) ∧
-  (inputSet _ = 0:num)
-End
-
-
-Definition out_signals_def:
-  out_signals prog =
-  let
-    tms = FLAT (MAP SND prog)
-  in
-    MAP num_to_str (terms_out_signals tms)
-End
-
-val _ = export_theory();
diff --git a/pancake/time_to_panScript.sml b/pancake/time_to_panScript.sml
deleted file mode 100644
index 3526619e12..0000000000
--- a/pancake/time_to_panScript.sml
+++ /dev/null
@@ -1,341 +0,0 @@
-(*
-  Compilation from timeLang to panLang
-*)
-
-open preamble pan_commonTheory mlintTheory
-     timeLangTheory panLangTheory
-
-val _ = new_theory "time_to_pan"
-
-val _ = set_grammar_ancestry
-        ["pan_common", "mlint", "timeLang", "panLang"];
-
-
-Definition ohd_def:
-  (ohd [] = (0:num,[])) ∧
-  (ohd (x::xs) = x)
-End
-
-
-Definition ffiBufferAddr_def:
-  ffiBufferAddr = 4000w:'a word
-End
-
-
-Definition ffiBufferSize_def:
-  ffiBufferSize =  (bytes_in_word + bytes_in_word): 'a word
-End
-
-
-Definition genShape_def:
-  genShape n = Comb (REPLICATE n One)
-End
-
-
-Definition mkClks_def:
-  mkClks vname n = REPLICATE n (Var vname)
-End
-
-
-Definition emptyConsts_def:
-  emptyConsts n = REPLICATE n (Const 0w)
-End
-
-
-Definition indicesOf_def:
-  indicesOf xs ys = MAP (λn. findi n xs) ys
-End
-
-
-Definition resetTermClocks_def:
-  resetTermClocks v clks tclks =
-  MAPi (λn e.
-         if (MEM e tclks)
-         then (Const 0w)
-         else Field n (Var v))
-       clks
-End
-
-
-Definition waitTimes_def:
-  waitTimes =
-    list$MAP2 (λt e. Op Sub [Const (n2w t); e])
-End
-
-
-Definition minOp_def:
-  (minOp v [] = Skip) ∧
-  (minOp v (e::es) =
-    Seq (If (Cmp Lower e (Var v)) (Assign v e) Skip)
-        (minOp v es))
-End
-
-
-Definition minExp_def:
-  (minExp v [] = Skip) ∧
-  (minExp v (e::es) = Seq (Assign v e) (minOp v es))
-End
-
-
-Definition compTerm_def:
-  (compTerm (clks:mlstring list) (Tm io cnds tclks loc wt)) : 'a prog =
-  let waitClks = indicesOf clks (MAP SND wt);
-      return   = Return
-                 (Struct
-                  [Var «newClks»;  Var «waitSet»;
-                   Var «wakeUpAt»; Label (num_to_str loc)])
-  in
-    decs [
-        («waitSet»,   case wt of [] => Const 1w | wt => Const 0w); (* not waitSet *)
-        («wakeUpAt»,  Const 0w);
-        («newClks»,   Struct (resetTermClocks «clks» clks tclks));
-        («waitTimes», Struct (emptyConsts (LENGTH wt)))
-      ]
-         (nested_seq
-          [Assign «waitTimes»
-                  (Struct (
-                    waitTimes
-                     (MAP FST wt)
-                     (MAP (λn. Field n (Var «newClks»)) waitClks)));
-           minExp «wakeUpAt» (MAPi (λn wt. Field n (Var «waitTimes»)) wt);
-           case io of
-           | (Input insig)   => return
-           | (Output outsig) =>
-               decs
-               [(«ptr1»,Const 0w);
-                («len1»,Const 0w);
-                («ptr2»,BaseAddr (* Const ffiBufferAddr *));
-                («len2»,Const ffiBufferSize)
-               ] (Seq
-                  (ExtCall (num_to_str outsig) (Var «ptr1») (Var «len1») (Var «ptr2») (Var «len2»))
-                  return)
-          ])
-End
-
-
-Definition compExp_def:
-  (compExp _ _ (ELit t) = Const (n2w t)) ∧
-  (compExp clks vname (EClock clk) =
-     Field (findi clk clks) (Var vname)) ∧
-  (compExp clks vname (ESub e1 e2) =
-     Op Sub [compExp clks vname e1;
-             compExp clks vname e2])
-End
-
-Definition compCondition_def:
-  (compCondition clks vname (CndLt e1 e2) =
-     Cmp Lower
-         (compExp clks vname e1)
-         (compExp clks vname e2)) ∧
-  (compCondition clks vname (CndLe e1 e2) =
-     Op Or [Cmp Lower
-                (compExp clks vname e1)
-                (compExp clks vname e2);
-            Cmp Equal
-                (compExp clks vname e1)
-                (compExp clks vname e2)])
-End
-
-Definition compConditions_def:
-  (compConditions clks vname [] = Const 1w) ∧
-  (compConditions clks vname cs =
-     Op And (MAP (compCondition clks vname) cs))
-End
-
-
-Definition compAction_def:
-  (compAction (Output _) = Const 0w) ∧
-  (compAction (Input n)  = Const (n2w (n + 1)))
-End
-
-
-Definition event_match_def:
-  event_match vname act = Cmp Equal (Var vname) (compAction act)
-End
-
-
-Definition pick_term_def:
-  pick_term clks cname ename cds act =
-    Op And
-       [compConditions clks cname cds;
-        event_match ename act]
-End
-
-Definition compTerms_def:
-  (compTerms clks cname ename [] = Raise «panic» (Const 0w)) ∧
-  (compTerms clks cname ename (t::ts) =
-   let
-     cds = termConditions t;
-     act = termAction t
-   in
-     If (pick_term clks cname ename cds act)
-     (compTerm clks t)
-     (compTerms clks cname ename ts))
-End
-
-Definition compLocation_def:
-  compLocation clks (loc,ts) =
-  let n = LENGTH clks in
-    (num_to_str loc,
-     [(«clks», genShape n);
-      («event», One)],
-     compTerms clks «clks» «event» ts)
-End
-
-Definition compProg_def:
-  (compProg clks [] = []) ∧
-  (compProg clks (p::ps) =
-    compLocation clks p :: compProg clks ps)
-End
-
-Definition comp_def:
-  comp prog =
-    compProg (clksOf prog) prog
-End
-
-
-Definition fieldsOf_def:
-  fieldsOf e n =
-    MAP (λn. Field n e) (GENLIST I n)
-End
-
-
-Definition normalisedClks_def:
-  normalisedClks v1 v2 n =
-  MAP2 (λx y. Op Sub [x;y])
-       (mkClks v1 n)
-       (fieldsOf (Var v2) n)
-End
-
-
-Definition check_input_time_def:
-  check_input_time =
-  let time =  Load One (Var «ptr2»);
-      input = Load One
-                   (Op Add [Var «ptr2»;
-                            Const bytes_in_word])
-  in
-    nested_seq [
-        ExtCall «get_time_input» (Var «ptr1») (Var «len1») (Var «ptr2») (Var «len2») ;
-        Assign  «sysTime» time ;
-        Assign  «event»   input;
-        Assign  «isInput» (Cmp Equal input (Const 0w));
-        If (Cmp Equal (Var «sysTime») (Const (n2w (dimword (:α) - 1))))
-           (Return (Const 0w)) (Skip:'a prog)
-      ]
-End
-
-Definition wait_def:
-  wait =
-    Op And [Var «isInput»; (* Not *)
-            Op Or
-            [Var «waitSet»; (* Not *)
-             Cmp NotEqual (Var «sysTime») (Var «wakeUpAt»)]]
-End
-
-Definition wait_input_time_limit_def:
-  wait_input_time_limit =
-    While wait check_input_time
-End
-
-Definition task_controller_def:
-  task_controller clksLength =
-  let
-    rt = Var «taskRet» ;
-    nClks     = Field 0 rt;
-    nWaitSet  = Field 1 rt;
-    nwakeUpAt = Field 2 rt;
-    nloc      = Field 3 rt
-  in
-    (nested_seq [
-        wait_input_time_limit;
-        If (Cmp Equal (Var «sysTime») (Const (n2w (dimword (:α) - 2))))
-           check_input_time (Skip:'a prog);
-        Call (SOME (SOME «taskRet», NONE)) (Var «loc»)
-             [Struct (normalisedClks «sysTime» «clks» clksLength);
-             Var «event»];
-        Assign «clks» nClks;
-        Assign «clks» (Struct (normalisedClks «sysTime» «clks» clksLength));
-        Assign «waitSet» nWaitSet ;
-        Assign «wakeUpAt» (Op Add [Var «sysTime»; nwakeUpAt]);
-        Assign «loc» nloc;
-        Assign «isInput» (Const 1w);
-        Assign «event» (Const 0w)])
-End
-
-
-Definition always_def:
-  always clksLength =
-  While (Const 1w)
-        (task_controller clksLength)
-End
-
-Definition start_controller_def:
-  start_controller (ta_prog:program) =
-  let
-    prog = FST ta_prog;
-    initLoc = FST (ohd prog);
-    initWakeUp = SND ta_prog;
-    clksLength = nClks prog
-  in
-    decs
-    [(«loc», Label (num_to_str initLoc));
-     («waitSet»,
-      case initWakeUp of NONE => Const 1w | _ => Const 0w);  (* not waitSet *)
-     («event», Const 0w);
-     («isInput», Const 1w); (* not isInput, active low *)
-     («wakeUpAt», Const 0w);
-     («sysTime», Const 0w);
-     («ptr1», Const 0w);
-     («len1», Const 0w);
-     («ptr2», BaseAddr (* Const ffiBufferAddr) *));
-     («len2», Const ffiBufferSize);
-     («taskRet»,
-      Struct [Struct (emptyConsts clksLength);
-              Const 0w; Const 0w; Label (num_to_str initLoc)]);
-     («clks»,Struct (emptyConsts clksLength))
-    ]
-    (nested_seq
-     [
-       check_input_time;
-       Assign «clks» (Struct (mkClks «sysTime» clksLength));
-       Assign «wakeUpAt»
-              (case initWakeUp of
-               | NONE => Var «sysTime»
-               | SOME n => Op Add [Var «sysTime»; Const (n2w n)]);
-       always clksLength
-     ])
-End
-
-
-Definition ta_controller_def:
-  ta_controller (ta_prog:program) =
-  decs
-  [
-    («retvar», Const 0w);
-    («excpvar», Const 0w)
-  ]
-  (nested_seq
-   [
-     Call (SOME (SOME «retvar»,
-           (SOME («panic», «excpvar», (Return (Const 1w))))))
-     (Label «start_controller»)
-     [];
-     Return (Const 0w)
-   ])
-End
-
-
-
-Definition compile_prog_def:
-  compile_prog prog =
-    let i = («start»,[],start_controller prog) in
-    let clks = clksOf (FST prog) in
-    let n = LENGTH clks in
-      i :: MAP (λ(loc,tms).
-            (num_to_str loc,
-             [(«clks», genShape n); («event», One)],
-             compTerms clks «clks» «event» tms)) (FST prog)
-End
-
-val _ = export_theory();
diff --git a/pancake/time_to_targetScript.sml b/pancake/time_to_targetScript.sml
deleted file mode 100644
index 3f1413c038..0000000000
--- a/pancake/time_to_targetScript.sml
+++ /dev/null
@@ -1,17 +0,0 @@
-(*
-  Compiler from timeLang to machine code
-*)
-
-open preamble
-     time_to_panTheory pan_to_targetTheory;
-
-val _ = new_theory "time_to_target";
-
-Definition compile_prog_def:
-  compile_prog c prog =
-    let prog = time_to_pan$compile_prog prog in
-    let prog = MAP (\(n,p,b). (n,F,p,b)) prog in
-      pan_to_target$compile_prog c prog
-End
-
-val _ = export_theory();