Mercurial Mercurial > repos > isabelle / 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.
src/HOL/NumberTheory/WilsonBij.thy
changeset 23894 1a4167d761ac
parent 21404 eb85850d3eb7
child 30042 31039ee583fa 
--- a/src/HOL/NumberTheory/WilsonBij.thy	Sat Jul 21 17:40:40 2007 +0200
+++ b/src/HOL/NumberTheory/WilsonBij.thy	Sat Jul 21 23:25:00 2007 +0200
@@ -150,7 +150,7 @@
         apply (rule_tac [7] zcong_trans)
          apply (tactic {* stac (thm "zcong_sym") 8 *})
          apply (erule_tac [7] inv_is_inv)
-          apply (tactic "Asm_simp_tac 9")
+          apply (tactic "asm_simp_tac @{simpset} 9")
           apply (erule_tac [9] inv_is_inv)
            apply (rule_tac [6] zless_zprime_imp_zrelprime)
              apply (rule_tac [8] inv_less)
isabelle