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.
isatool unsymbolize;
authorwenzelm
Thu, 15 Nov 2001 23:21:57 +0100
changeset 12216 dda8c04a8fb4
parent 12215 55c084921240
child 12217 e3efc5c9f267
isatool unsymbolize;
src/ZF/Induct/Term.thy file | annotate | diff | comparison | revisions
src/ZF/Induct/Tree_Forest.thy file | annotate | diff | comparison | revisions 
--- 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)"
--- 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
isabelle