--- a/Quot/Examples/AbsRepTest.thy Mon Feb 15 14:58:03 2010 +0100
+++ b/Quot/Examples/AbsRepTest.thy Mon Feb 15 16:28:07 2010 +0100
@@ -8,49 +8,6 @@
ML_command "ProofContext.verbose := false"
*)
-ML {*
-val ctxt0 = @{context}
-val ty = Syntax.read_typ ctxt0 "bool"
-val ctxt1 = Variable.declare_typ ty ctxt0
-val trm = Syntax.parse_term ctxt1 "A \<and> B"
-val trm' = Syntax.type_constraint ty trm
-val trm'' = Syntax.check_term ctxt1 trm'
-val ctxt2 = Variable.declare_term trm'' ctxt1
-*}
-
-term "split"
-
-term "Ex1 (\<lambda>(x, y). P x y)"
-
-lemma "(Ex1 (\<lambda>(x, y). P x y)) \<Longrightarrow> (\<exists>! x. \<exists>! y. P x y)"
-apply(erule ex1E)
-apply(case_tac x)
-apply(clarify)
-apply(rule_tac a="aa" in ex1I)
-apply(rule ex1I)
-apply(assumption)
-apply(blast)
-apply(blast)
-done
-
-(*
-lemma "(\<exists>! x. \<exists>! y. P x y) \<Longrightarrow> (Ex1 (\<lambda>(x, y). P x y))"
-apply(erule ex1E)
-apply(erule ex1E)
-apply(rule_tac a="(x, y)" in ex1I)
-apply(clarify)
-apply(case_tac xa)
-apply(clarify)
-
-apply(rule ex1I)
-apply(assumption)
-apply(blast)
-apply(blast)
-done
-
-apply(metis)
-*)
-
ML {* open Quotient_Term *}
ML {*