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/Old_Number_Theory/WilsonBij.thy
changeset 51717 9e7d1c139569
parent 47268 262d96552e50
child 57418 6ab1c7cb0b8d 
--- a/src/HOL/Old_Number_Theory/WilsonBij.thy	Tue Apr 16 17:54:14 2013 +0200
+++ b/src/HOL/Old_Number_Theory/WilsonBij.thy	Thu Apr 18 17:07:01 2013 +0200
@@ -143,7 +143,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 @{simpset} 9")
+          apply (tactic "asm_simp_tac @{context} 9")
           apply (erule_tac [9] inv_is_inv)
            apply (rule_tac [6] zless_zprime_imp_zrelprime)
              apply (rule_tac [8] inv_less)
isabelle