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.
IntEx.thy
changeset 558 114bb544ecb9
parent 557 e67961288b12
child 559 d641c32855f0 
--- a/IntEx.thy	Sat Dec 05 21:45:56 2009 +0100
+++ b/IntEx.thy	Sat Dec 05 21:47:48 2009 +0100
@@ -176,7 +176,6 @@
 apply(rule ballI)
 apply(rule apply_rsp[OF Quotient_my_int ho_plus_rsp])
 apply(simp only: in_respects)
-
 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
@@ -196,9 +195,6 @@
 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 apply(fold PLUS_def)
 apply(tactic {* clean_tac @{context} 1 *})
-thm Quotient_rel_rep
-thm Quotient_rel_rep[OF fun_quotient[OF Quotient_my_int Quotient_my_int]]
-apply(simp only: Quotient_rel_rep[OF fun_quotient[OF Quotient_my_int Quotient_my_int]])
 done
 
 lemma test3: "my_plus = my_plus"
@@ -217,7 +213,6 @@
 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 apply(tactic {* clean_tac @{context} 1 *})
-apply(simp only: Quotient_rel_rep[OF fun_quotient[OF Quotient_my_int fun_quotient[OF Quotient_my_int Quotient_my_int]]])
 done
nominal2