Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merged
authorChristian Urban <urbanc@in.tum.de>
Thu, 03 Dec 2009 11:34:34 +0100
changeset 494 abafefa0d58b
parent 493 672b94510e7d
child 495 76fa93b1fe8b
child 502 6b2f6e7e62cc
merged
IntEx.thy file | annotate | diff | comparison | revisions 
--- a/IntEx.thy	Thu Dec 03 11:33:24 2009 +0100
+++ b/IntEx.thy	Thu Dec 03 11:34:34 2009 +0100
@@ -285,8 +285,6 @@
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 apply(simp only: foldl_prs[OF QUOTIENT_my_int QUOTIENT_my_int])
 apply(simp only: nil_prs)
-apply(rule test_all_prs)
-apply(tactic {* rtac quot 1 *})
 apply(tactic {* clean_tac @{context} [quot] defs 1 *})
 done
nominal2