# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1255600590 -7200
# Node ID 41a2ab50dd890ba6cadf3963ca876819aaff969f
# Parent  4aef3882b436a263fe86f72c87fd065c0a1649de
Cleaning the proofs

diff -r 4aef3882b436 -r 41a2ab50dd89 QuotMain.thy
--- a/QuotMain.thy	Thu Oct 15 11:55:52 2009 +0200
+++ b/QuotMain.thy	Thu Oct 15 11:56:30 2009 +0200
@@ -1054,11 +1054,7 @@
   apply (rule RIGHT_RES_FORALL_REGULAR)
   prefer 2
   apply (assumption)
-  apply (auto)
-  apply (rule allI)
-  apply (rule impI)
-  apply (rule impI)
-  apply (assumption)
+  apply (metis)
   done
 
 ML {* val li = Thm.freezeT (atomize_thm @{thm card1_suc}) *}
@@ -1067,11 +1063,9 @@
  Logic.mk_implies
    ((prop_of li),
    (regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context})) *}
-  apply (simp only: equiv_res_forall[OF equiv_list_eq])
-  apply (simp only: equiv_res_exists[OF equiv_list_eq])
+  apply (simp add: equiv_res_forall[OF equiv_list_eq] equiv_res_exists[OF equiv_list_eq])
   done
 
-thm card1_suc
 ML {* @{thm card1_suc_r} OF [li] *}
 
 ML {* val li = Thm.freezeT (atomize_thm @{thm fold1.simps(2)}) *}