diff -r c3913a79b6ae -r 492493334e0f ex/Simult.thy
--- a/ex/Simult.thy	Fri Apr 14 11:23:33 1995 +0200
+++ b/ex/Simult.thy	Wed Jun 21 15:12:40 1995 +0200
@@ -31,12 +31,12 @@
   Tcons       :: "['a, 'a forest] => 'a tree"
   Fcons       :: "['a tree, 'a forest] => 'a forest"
   Fnil        :: "'a forest"
-  TF_rec      :: "['a item, ['a item , 'a item, 'b]=>'b,     \
-\                 'b, ['a item , 'a item, 'b, 'b]=>'b] => 'b"
-  tree_rec    :: "['a tree, ['a, 'a forest, 'b]=>'b,          \
-\                 'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b"
-  forest_rec  :: "['a forest, ['a, 'a forest, 'b]=>'b,        \
-\                  'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b"
+  TF_rec      :: "['a item, ['a item , 'a item, 'b]=>'b,     
+                 'b, ['a item , 'a item, 'b, 'b]=>'b] => 'b"
+  tree_rec    :: "['a tree, ['a, 'a forest, 'b]=>'b,          
+                 'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b"
+  forest_rec  :: "['a forest, ['a, 'a forest, 'b]=>'b,        
+                  'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b"
 
 defs
      (*the concrete constants*)
@@ -48,8 +48,8 @@
   Fnil_def  	"Fnil        == Abs_Forest(FNIL)"
   Fcons_def 	"Fcons(t,ts) == Abs_Forest(FCONS(Rep_Tree(t), Rep_Forest(ts)))"
 
-  TF_def	"TF(A) == lfp(%Z. A <*> Part(Z,In1) \
-\                           <+> ({Numb(0)} <+> Part(Z,In0) <*> Part(Z,In1)))"
+  TF_def	"TF(A) == lfp(%Z. A <*> Part(Z,In1) 
+                           <+> ({Numb(0)} <+> Part(Z,In0) <*> Part(Z,In1)))"
 
 rules
   (*faking a type definition for tree...*)
@@ -66,17 +66,17 @@
 defs
      (*recursion*)
   TF_rec_def	
-   "TF_rec(M,b,c,d) == wfrec(trancl(pred_sexp), M, 			\
-\               Case(Split(%x y g. b(x,y,g(y))),		\
-\	              List_case(%g.c, %x y g. d(x,y,g(x),g(y)))))"
+   "TF_rec(M,b,c,d) == wfrec(trancl(pred_sexp), M, 			
+               Case(Split(%x y g. b(x,y,g(y))),		
+	              List_case(%g.c, %x y g. d(x,y,g(x),g(y)))))"
 
   tree_rec_def
-   "tree_rec(t,b,c,d) == \
-\   TF_rec(Rep_Tree(t), %x y r. b(Inv(Leaf,x), Abs_Forest(y), r), \
-\          c, %x y rt rf. d(Abs_Tree(x), Abs_Forest(y), rt, rf))"
+   "tree_rec(t,b,c,d) == 
+   TF_rec(Rep_Tree(t), %x y r. b(Inv(Leaf,x), Abs_Forest(y), r), 
+          c, %x y rt rf. d(Abs_Tree(x), Abs_Forest(y), rt, rf))"
 
   forest_rec_def
-   "forest_rec(tf,b,c,d) == \
-\   TF_rec(Rep_Forest(tf), %x y r. b(Inv(Leaf,x), Abs_Forest(y), r), \
-\          c, %x y rt rf. d(Abs_Tree(x), Abs_Forest(y), rt, rf))"
+   "forest_rec(tf,b,c,d) == 
+   TF_rec(Rep_Forest(tf), %x y r. b(Inv(Leaf,x), Abs_Forest(y), r), 
+          c, %x y rt rf. d(Abs_Tree(x), Abs_Forest(y), rt, rf))"
 end