# HG changeset patch
# User wenzelm
# Date 1005862917 -3600
# Node ID dda8c04a8fb49d15819725abd31a0f332efa4b2f
# Parent  55c0849212401aa2d675ffcf25dd4201c1e82254
isatool unsymbolize;

diff -r 55c084921240 -r dda8c04a8fb4 src/ZF/Induct/Term.thy
--- a/src/ZF/Induct/Term.thy	Thu Nov 15 20:01:19 2001 +0100
+++ b/src/ZF/Induct/Term.thy	Thu Nov 15 23:21:57 2001 +0100
@@ -167,7 +167,7 @@
 *}
 
 lemma term_map [simp]:
-    "ts \<in> list(A) \<Longrightarrow> term_map(f, Apply(a, ts)) = Apply(f(a), map(term_map(f), ts))"
+    "ts \<in> list(A) ==> term_map(f, Apply(a, ts)) = Apply(f(a), map(term_map(f), ts))"
   by (rule term_map_def [THEN def_term_rec])
 
 lemma term_map_type [TC]:
@@ -188,7 +188,7 @@
 *}
 
 lemma term_size [simp]:
-    "ts \<in> list(A) \<Longrightarrow> term_size(Apply(a, ts)) = succ(list_add(map(term_size, ts)))"
+    "ts \<in> list(A) ==> term_size(Apply(a, ts)) = succ(list_add(map(term_size, ts)))"
   by (rule term_size_def [THEN def_term_rec])
 
 lemma term_size_type [TC]: "t \<in> term(A) ==> term_size(t) \<in> nat"
@@ -200,7 +200,7 @@
 *}
 
 lemma reflect [simp]:
-    "ts \<in> list(A) \<Longrightarrow> reflect(Apply(a, ts)) = Apply(a, rev(map(reflect, ts)))"
+    "ts \<in> list(A) ==> reflect(Apply(a, ts)) = Apply(a, rev(map(reflect, ts)))"
   by (rule reflect_def [THEN def_term_rec])
 
 lemma reflect_type [TC]: "t \<in> term(A) ==> reflect(t) \<in> term(A)"
@@ -212,7 +212,7 @@
 *}
 
 lemma preorder [simp]:
-    "ts \<in> list(A) \<Longrightarrow> preorder(Apply(a, ts)) = Cons(a, flat(map(preorder, ts)))"
+    "ts \<in> list(A) ==> preorder(Apply(a, ts)) = Cons(a, flat(map(preorder, ts)))"
   by (rule preorder_def [THEN def_term_rec])
 
 lemma preorder_type [TC]: "t \<in> term(A) ==> preorder(t) \<in> list(A)"
@@ -224,7 +224,7 @@
 *}
 
 lemma postorder [simp]:
-    "ts \<in> list(A) \<Longrightarrow> postorder(Apply(a, ts)) = flat(map(postorder, ts)) @ [a]"
+    "ts \<in> list(A) ==> postorder(Apply(a, ts)) = flat(map(postorder, ts)) @ [a]"
   by (rule postorder_def [THEN def_term_rec])
 
 lemma postorder_type [TC]: "t \<in> term(A) ==> postorder(t) \<in> list(A)"
diff -r 55c084921240 -r dda8c04a8fb4 src/ZF/Induct/Tree_Forest.thy
--- a/src/ZF/Induct/Tree_Forest.thy	Thu Nov 15 20:01:19 2001 +0100
+++ b/src/ZF/Induct/Tree_Forest.thy	Thu Nov 15 23:21:57 2001 +0100
@@ -20,10 +20,10 @@
 
 declare tree_forest.intros [simp, TC]
 
-lemma tree_def: "tree(A) \<equiv> Part(tree_forest(A), Inl)"
+lemma tree_def: "tree(A) == Part(tree_forest(A), Inl)"
   by (simp only: tree_forest.defs)
 
-lemma forest_def: "forest(A) \<equiv> Part(tree_forest(A), Inr)"
+lemma forest_def: "forest(A) == Part(tree_forest(A), Inr)"
   by (simp only: tree_forest.defs)
 
 
@@ -234,7 +234,8 @@
     apply simp_all
   done
 
-lemma map_compose: "z \<in> tree_forest(A) ==> map(h, map(j,z)) = map(\<lambda>u. h(j(u)), z)"
+lemma map_compose:
+    "z \<in> tree_forest(A) ==> map(h, map(j,z)) = map(\<lambda>u. h(j(u)), z)"
   apply (erule tree_forest.induct)
     apply simp_all
   done