Mercurial Mercurial > repos > isabelle / 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.
omit automatic Induct.cases_pred declaration, which breaks many existing proofs
authorkrauss
Thu, 12 Sep 2013 22:10:17 +0200
changeset 53614 8c51fc24d83c
parent 53613 cdc780645a49
child 53615 f557a4645f61
omit automatic Induct.cases_pred declaration, which breaks many existing proofs
src/HOL/Tools/Function/function.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Function/function.ML	Tue Sep 10 20:34:32 2013 +0200
+++ b/src/HOL/Tools/Function/function.ML	Thu Sep 12 22:10:17 2013 +0200
@@ -211,7 +211,7 @@
            ((qualify "induct",
              [Attrib.internal (K (Rule_Cases.case_names case_names))]),
             tinduct)
-        ||>> fold_map (note_qualified "elims" [Rule_Cases.consumes 1, Rule_Cases.constraints 1, Induct.cases_pred defname]) (fnames ~~ telims)
+        ||>> fold_map (note_qualified "elims" [Rule_Cases.consumes 1, Rule_Cases.constraints 1]) (fnames ~~ telims)
         |-> (fn ((simps,(_,inducts)), elims) => fn lthy =>
           let val info' = { is_partial=false, defname=defname, fnames=fnames, add_simps=add_simps,
             case_names=case_names, fs=fs, R=R, dom=dom, psimps=psimps, pinducts=pinducts,
isabelle