# HG changeset patch
# User wenzelm
# Date 1433674542 -7200
# Node ID b35b08a143b2c0716c9490d5e39d16fa068bb27d
# Parent  6b858199f240af5677c03fc4364dfb16b8005ea2
tuned;

diff -r 6b858199f240 -r b35b08a143b2 src/FOLP/ex/Classical.thy
--- a/src/FOLP/ex/Classical.thy	Sun Jun 07 12:55:28 2015 +0200
+++ b/src/FOLP/ex/Classical.thy	Sun Jun 07 12:55:42 2015 +0200
@@ -286,9 +286,8 @@
   by (tactic "fast_tac @{context} FOLP_cs 1")
 
 text "Problem 58  NOT PROVED AUTOMATICALLY"
-schematic_lemma
-  notes f_cong = subst_context [where t = f]
-  shows "?p : (ALL x y. f(x)=g(y)) --> (ALL x y. f(f(x))=f(g(y)))"
+schematic_lemma "?p : (ALL x y. f(x)=g(y)) --> (ALL x y. f(f(x))=f(g(y)))"
+  supply f_cong = subst_context [where t = f]
   by (tactic {* fast_tac @{context} (FOLP_cs addSIs [@{thm f_cong}]) 1 *})
 
 text "Problem 59"
diff -r 6b858199f240 -r b35b08a143b2 src/ZF/Induct/Tree_Forest.thy
--- a/src/ZF/Induct/Tree_Forest.thy	Sun Jun 07 12:55:28 2015 +0200
+++ b/src/ZF/Induct/Tree_Forest.thy	Sun Jun 07 12:55:42 2015 +0200
@@ -59,12 +59,10 @@
   apply (auto intro!: equalityI tree_forest.intros elim: tree_forest.cases)
   done
 
-lemma
-  notes rews = tree_forest.con_defs tree_def forest_def
-  shows
-    tree_forest_unfold: "tree_forest(A) =
-      (A \<times> forest(A)) + ({0} + tree(A) \<times> forest(A))"
+lemma tree_forest_unfold:
+  "tree_forest(A) = (A \<times> forest(A)) + ({0} + tree(A) \<times> forest(A))"
     -- {* NOT useful, but interesting \dots *}
+  supply rews = tree_forest.con_defs tree_def forest_def
   apply (unfold tree_def forest_def)
   apply (fast intro!: tree_forest.intros [unfolded rews, THEN PartD1]
     elim: tree_forest.cases [unfolded rews])