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.
Now applies standard' to "unfold" theorem (due to flex-flex constraints).
authorberghofe
Mon, 21 Oct 2002 17:00:45 +0200
changeset 13657 c1637d60a846
parent 13656 58bb243dbafb
child 13658 c9ad3e64ddcf
Now applies standard' to "unfold" theorem (due to flex-flex constraints).
src/HOL/Tools/inductive_package.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/inductive_package.ML	Mon Oct 21 16:57:39 2002 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Mon Oct 21 17:00:45 2002 +0200
@@ -491,7 +491,7 @@
   let
     val _ = clean_message "  Proving the introduction rules ...";
 
-    val unfold = standard (mono RS (fp_def RS
+    val unfold = standard' (mono RS (fp_def RS
       (if coind then def_gfp_unfold else def_lfp_unfold)));
 
     fun select_disj 1 1 = []
isabelle