--- a/progtut/Tactical.thy~	Sat Sep 13 10:07:14 2014 +0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,76 +0,0 @@
-theory Tactical
-imports Advanced
-begin
-
-
-
-
-ML {*
-fun my_print_tac ctxt thm =
-let
-   val _ = tracing (Pretty.string_of (pretty_thm_no_vars ctxt thm))
-in
-   Seq.single thm
-end
-*}
-
-ML {*
-let
-   val ctxt = @{context}
-   val goal = @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"}
-in
-   Goal.prove ctxt ["x", "y", "u", "v", "P", "Q"] [@{prop "x = y"}, @{prop "u = v"}] goal
-    (fn {prems = pms, context = ctxt} =>  
-              (my_print_tac ctxt)
-              THEN etac @{thm disjE} 1 THEN
-               (my_print_tac ctxt) 
-              THEN rtac @{thm disjI2} 1
-              THEN  (my_print_tac ctxt) 
-              THEN atac 1
-              THEN rtac @{thm disjI1} 1
-              THEN atac 1)
-end
-*}
-
-ML {*
-  Goal.prove
-*}
-
-ML {*
-fun pretty_cterms ctxt ctrms =
-  Pretty.block (Pretty.commas (map (pretty_cterm ctxt) ctrms))
-*}
-
-ML {*
-fun foc_tac {prems, params, asms, concl, context, schematics} =
-let
-  fun assgn1 f1 f2 xs =
-    let
-       val out = map (fn (x, y) => Pretty.enum ":=" "" "" [f1 x, f2 y]) xs
-    in
-       Pretty.list "" "" out
-    end
-  fun assgn2 f xs = assgn1 f f xs
-  val pps = map (fn (s, pp) => Pretty.block [Pretty.str s, pp])
-    [("params: ", assgn1 Pretty.str (pretty_cterm context) params),
-     ("assumptions: ", pretty_cterms context asms),
-     ("conclusion: ", pretty_cterm context concl),
-     ("premises: ", pretty_thms_no_vars context prems),
-     ("schematics: ", assgn2 (pretty_cterm context) (snd schematics))]
-in
-  tracing (Pretty.string_of (Pretty.chunks pps)); all_tac
-end
-*}
-
-
-notation (output) "prop"   ("#_" [1000] 1000)
-
-lemma
-  shows " \<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"
-apply(tactic {* my_print_tac @{context} *})
-apply(rule conjI)
-apply(tactic {* my_print_tac @{context} *})
-apply(assumption)
-apply(tactic {* my_print_tac @{context} *})
-apply(assumption)
-apply(tactic {* my_print_tac @{context} *})