--- a/progtut/FirstStep.thy~	Sat Sep 13 10:07:14 2014 +0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,173 +0,0 @@
-theory FistStep
-imports Main
-begin
-
-ML {*
-val pretty_term = Syntax.pretty_term
-val pwriteln = Pretty.writeln
-fun pretty_terms ctxt trms =
-  Pretty.block (Pretty.commas (map (pretty_term ctxt) trms))
-val show_type_ctxt = Config.put show_types true @{context}
-val show_all_types_ctxt = Config.put show_all_types true @{context}
-fun pretty_cterm ctxt ctrm =
-  pretty_term ctxt (term_of ctrm)
-fun pretty_thm ctxt thm =
-  pretty_term ctxt (prop_of thm)
-fun pretty_thm_no_vars ctxt thm =
-let
-  val ctxt' = Config.put show_question_marks false ctxt
-in
-  pretty_term ctxt' (prop_of thm)
-end
-fun pretty_thms ctxt thms =
-  Pretty.block (Pretty.commas (map (pretty_thm ctxt) thms))
-fun pretty_thms_no_vars ctxt thms =
-  Pretty.block (Pretty.commas (map (pretty_thm_no_vars ctxt) thms))
-fun pretty_typ ctxt ty = Syntax.pretty_typ ctxt ty
-fun pretty_typs ctxt tys =
-  Pretty.block (Pretty.commas (map (pretty_typ ctxt) tys))
-fun pretty_ctyp ctxt cty = pretty_typ ctxt (typ_of cty)
-fun pretty_ctyps ctxt ctys =
-  Pretty.block (Pretty.commas (map (pretty_ctyp ctxt) ctys))
-fun `f = fn x => (f x, x)
-fun (x, y) |>> f = (f x, y)
-fun (x, y) ||> f = (x, f y)
-fun (x, y) |-> f = f x y
-*}
-
-ML {*
-  val _ = pretty_term @{context} @{term "x + y + z"} |> pwriteln
-  val _ = pretty_terms @{context} [@{term "x + y"}, @{term "x + y + z"}] |> pwriteln
-  val show_type_ctxt = Config.put show_types true @{context}
-  *}
-
-ML {*
-   pwriteln (pretty_term show_type_ctxt @{term "(1::nat, x)"})
-*}
-
-ML {*
-pwriteln (Pretty.str (cat_lines ["foo", "bar"]))
-*}
-
-ML {*
-  fun apply_fresh_args f ctxt =
-      f |> fastype_of
-        |> binder_types
-        |> map (pair "z")
-        |> Variable.variant_frees ctxt [f]
-        |> map Free
-        |> tap (fn x => pwriteln (Pretty.str (@{make_string} x)))
-        |> curry list_comb f
-*}
-
-ML {*
-let
-   val trm = @{term "P::nat => int => unit => bool"}
-   val ctxt = ML_Context.the_local_context ()
-in
-   apply_fresh_args trm ctxt
-    |> pretty_term ctxt
-    |> pwriteln
-end
-*}
-
-ML {*
-  fun inc_by_three x =
-      x |> (fn x => x + 1)
-        |> tap (fn x => pwriteln (Pretty.str (@{make_string} x)))
-        |> (fn x => x + 2)
-*}
-
-ML {*
-  fun `f = fn x => (f x, x)
-*}
-
-ML {*
-  fun inc_as_pair x =
-        x |> `(fn x => x + 1)
-       |> (fn (x, y) => (x, y + 1))
-*}
-
-ML {*
-  3 |> inc_as_pair
-*}
-
-ML {*
-  fun acc_incs x =
-      x |> (fn x => (0, x))
-        ||>> (fn x => (x, x + 1))
-        ||>> (fn x => (x, x + 1))
-        ||>> (fn x => (x, x + 1))
-*}
-
-ML {*
-  2 |> acc_incs
-*}
-
-ML {*
-let
-  val ((names1, names2), _) =
-    @{context}
-    |> Variable.variant_fixes (replicate 4 "x")
-    |> tap (fn x => pwriteln (Pretty.str (@{make_string} x)))
-    ||>> Variable.variant_fixes (replicate 5 "x")
-    |> tap (fn x => pwriteln (Pretty.str (@{make_string} x)))
-in
-  (names1, names2)
-end
-*}
-
-ML {*
-  @{context}
-  |> Local_Defs.add_def ((@{binding "One"}, NoSyn), @{term "1::nat"})
-  ||>> Local_Defs.add_def ((@{binding "Two"}, NoSyn), @{term "2::nat"})
-  ||>> Local_Defs.add_def ((@{binding "Three"}, NoSyn), @{term "3::nat"})
-*}
-
-ML {*
-let
-   val ctxt = @{context}
-in
-   Syntax.parse_term ctxt "m + n"
-   |> singleton (Syntax.check_terms ctxt)
-   |> pretty_term ctxt
-   |> pwriteln
-end
-*}
-
-ML {*
-  val term_pat_setup =
-  let
-    val parser = Args.context -- Scan.lift Args.name_source
-      fun term_pat (ctxt, str) =
-         str |> Proof_Context.read_term_pattern ctxt
-             |> ML_Syntax.print_term
-             |> ML_Syntax.atomic
-   in
-      ML_Antiquote.inline @{binding "term_pat"} (parser >> term_pat)
-   end
-*}
-
-setup {* term_pat_setup *}
-
-
-ML {*
-val type_pat_setup =
-let
-   val parser = Args.context -- Scan.lift Args.name_source
-   fun typ_pat (ctxt, str) =
-     let
-       val ctxt' = Proof_Context.set_mode Proof_Context.mode_schematic ctxt
-     in
-       str |> Syntax.read_typ ctxt'
-           |> ML_Syntax.print_typ
-           |> ML_Syntax.atomic
-       end
-in
-   ML_Antiquote.inline @{binding "typ_pat"} (parser >> typ_pat)
-end
-*}
-
-setup {* type_pat_setup *}
-
-end
\ No newline at end of file