--- 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"
--- 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])