# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1254256548 -7200
# Node ID 13be92f5b6388c2788d3154592cd228d1ab6253b
# Parent  ec5fbe7ab427d5a5fc3f79213eead2e9b5259a61
used new cong_tac

diff -r ec5fbe7ab427 -r 13be92f5b638 Prove.thy
--- a/Prove.thy	Tue Sep 29 17:46:18 2009 +0200
+++ b/Prove.thy	Tue Sep 29 22:35:48 2009 +0200
@@ -16,16 +16,13 @@
     val trm = ML_Context.evaluate lthy true ("r", r) txt
   in
     Proof.theorem_i NONE (after_qed name_spec) [[(trm,[])]] lthy
-  end;
+  end
 
   val parser = SpecParse.opt_thm_name ":" -- OuterParse.ML_source
-
 in
   OuterSyntax.local_theory_to_proof "prove" "proving a proposition" 
     OuterKeyword.thy_goal (parser >> setup_proof)
 end
 *}
 
-
-
 end
diff -r ec5fbe7ab427 -r 13be92f5b638 QuotList.thy
--- a/QuotList.thy	Tue Sep 29 17:46:18 2009 +0200
+++ b/QuotList.thy	Tue Sep 29 22:35:48 2009 +0200
@@ -2,7 +2,6 @@
 imports QuotScript
 begin
 
-
 lemma LIST_map_I:
   shows "map (\<lambda>x. x) = (\<lambda>x. x)"
   by simp
diff -r ec5fbe7ab427 -r 13be92f5b638 QuotMain.thy
--- a/QuotMain.thy	Tue Sep 29 17:46:18 2009 +0200
+++ b/QuotMain.thy	Tue Sep 29 22:35:48 2009 +0200
@@ -975,6 +975,9 @@
   shows "(a \<equiv> b) \<Longrightarrow> (Trueprop a \<equiv> Trueprop b)"
   by auto
 
+ML {*
+  Cong_Tac.cong_tac
+*}
 
 thm QUOT_TYPE_I_fset.R_trans2
 ML {*
@@ -987,7 +990,7 @@
       rtac @{thm card1_rsp},
       rtac @{thm QUOT_TYPE_I_fset.R_trans2},
       CHANGED o (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})),
-      DatatypeAux.cong_tac,
+      Cong_Tac.cong_tac @{thm cong},
       rtac @{thm ext},
 (*      rtac @{thm eq_reflection},*)
       CHANGED o (ObjectLogic.full_atomize_tac)
@@ -1232,5 +1235,5 @@
 | UPDATE1 "obj1 \<Rightarrow> string \<Rightarrow> (string \<Rightarrow> obj1)"
 *)
 
-Random test line at the end
-A second line
+end
+