Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
QuotMain.thy
changeset 156 9c74171ff78b
parent 154 1610de61c44b
child 157 ca0b28863ca9 
--- a/QuotMain.thy	Thu Oct 22 15:44:16 2009 +0200
+++ b/QuotMain.thy	Thu Oct 22 15:45:05 2009 +0200
@@ -1035,7 +1035,7 @@
       instantiate_tac @{thm REP_ABS_RSP(1)} ctxt,
       instantiate_tac @{thm APPLY_RSP} ctxt,
       rtac reflex_thm,
-      Cong_Tac.cong_tac @{thm cong},
+(*      Cong_Tac.cong_tac @{thm cong},*)
       atac
     ])
 *}
@@ -1093,7 +1093,6 @@
 apply (rule allI)
 apply (rule impI)
 apply (tactic {* instantiate_tac @{thm RES_FORALL_RSP} @{context} 1 *})
-apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 apply (simp only: FUN_REL.simps)
 (* ABS_REP_RSP *)
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
@@ -1153,7 +1152,6 @@
 apply (rule allI)
 apply (rule impI)
 apply (tactic {* instantiate_tac @{thm RES_FORALL_RSP} @{context} 1 *})
-apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 apply (simp only: FUN_REL.simps)
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 apply (simp only: FUN_REL.simps)
@@ -1171,7 +1169,6 @@
 apply (rule allI)
 apply (rule impI)
 apply (tactic {* instantiate_tac @{thm RES_FORALL_RSP} @{context} 1 *})
-apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 apply (simp only: FUN_REL.simps)
 done
nominal2