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.
merged
authorhaftmann
Fri, 02 Jan 2009 15:35:11 +0100
changeset 29335 88d23c927e37
parent 29306 2c764235e041 (diff)
parent 29334 3eb95594ba89 (current diff)
child 29336 beb83f120fe8
merged
--- a/src/FOLP/IFOLP.thy	Fri Jan 02 08:15:24 2009 +0100
+++ b/src/FOLP/IFOLP.thy	Fri Jan 02 15:35:11 2009 +0100
@@ -339,6 +339,7 @@
   shows "?a : R"
   apply (insert assms(1) [unfolded ex1_def])
   apply (erule exE conjE | assumption | rule assms(1))+
+  apply (erule assms(2), assumption)
   done
 
 
--- a/src/ZF/Tools/inductive_package.ML	Fri Jan 02 08:15:24 2009 +0100
+++ b/src/ZF/Tools/inductive_package.ML	Fri Jan 02 15:35:11 2009 +0100
@@ -249,7 +249,7 @@
     |> ListPair.map (fn (t, tacs) =>
       Goal.prove_global thy1 [] [] t
         (fn _ => EVERY (rewrite_goals_tac part_rec_defs :: tacs)))
-    handle Simplifier.SIMPLIFIER (msg, thm) => (Display.print_thm thm; error msg);
+    handle MetaSimplifier.SIMPLIFIER (msg, thm) => (Display.print_thm thm; error msg);
 
   (********)
   val dummy = writeln "  Proving the elimination rule...";
isabelle