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/ZF/Tools/induct_tacs.ML
changeset 35409 5c5bb83f2bae
parent 33522 737589bb9bb8
child 36610 bafd82950e24 
--- a/src/ZF/Tools/induct_tacs.ML	Sat Feb 27 23:13:01 2010 +0100
+++ b/src/ZF/Tools/induct_tacs.ML	Sun Feb 28 22:30:51 2010 +0100
@@ -136,7 +136,7 @@
            rec_rewrites = recursor_eqns,
            case_rewrites = case_eqns,
            induct = induct,
-           mutual_induct = TrueI,  (*No need for mutual induction*)
+           mutual_induct = @{thm TrueI},  (*No need for mutual induction*)
            exhaustion = elim};
 
     val con_info =
isabelle