diff -r c3913a79b6ae -r 492493334e0f ex/MT.thy
--- a/ex/MT.thy	Fri Apr 14 11:23:33 1995 +0200
+++ b/ex/MT.thy	Wed Jun 21 15:12:40 1995 +0200
@@ -102,9 +102,9 @@
   e_var_inj "e_var(ev1) = e_var(ev2) ==> ev1 = ev2"
   e_fn_inj "fn ev1 => e1 = fn ev2 => e2 ==> ev1 = ev2 & e1 = e2"
   e_fix_inj 
-    " fix ev11e(v12) = e1 = fix ev21(ev22) = e2 ==> \
-\     ev11 = ev21 & ev12 = ev22 & e1 = e2 \
-\   "
+    " fix ev11e(v12) = e1 = fix ev21(ev22) = e2 ==>
+      ev11 = ev21 & ev12 = ev22 & e1 = e2
+    "
   e_app_inj "e11 @ e12 = e21 @ e22 ==> e11 = e21 & e12 = e22"
 
 (* All constructors are distinct *)
@@ -123,14 +123,14 @@
 (* Strong elimination, induction on expressions  *)
 
   e_ind 
-    " [|  !!ev. P(e_var(ev)); \
-\         !!c. P(e_const(c)); \
-\         !!ev e. P(e) ==> P(fn ev => e); \
-\         !!ev1 ev2 e. P(e) ==> P(fix ev1(ev2) = e); \
-\         !!e1 e2. P(e1) ==> P(e2) ==> P(e1 @ e2) \
-\     |] ==> \
-\   P(e) \
-\   "
+    " [|  !!ev. P(e_var(ev));
+          !!c. P(e_const(c));
+          !!ev e. P(e) ==> P(fn ev => e);
+          !!ev1 ev2 e. P(e) ==> P(fix ev1(ev2) = e);
+          !!e1 e2. P(e1) ==> P(e2) ==> P(e1 @ e2)
+      |] ==>
+    P(e)
+    "
 
 (* Types - same scheme as for expressions *)
 
@@ -144,8 +144,8 @@
 (* Strong elimination, induction on types *)
 
  t_ind 
-    "[| !!p. P(t_const(p)); !!t1 t2. P(t1) ==> P(t2) ==> P(t_fun(t1,t2)) |] \
-\    ==> P(t)"
+    "[| !!p. P(t_const(p)); !!t1 t2. P(t1) ==> P(t2) ==> P(t_fun(t1,t2)) |]
+     ==> P(t)"
 
 
 (* Values - same scheme again *)
@@ -154,8 +154,8 @@
 
   v_const_inj "v_const(c1) = v_const(c2) ==> c1 = c2"
   v_clos_inj 
-    " v_clos(<|ev1,e1,ve1|>) = v_clos(<|ev2,e2,ve2|>) ==> \
-\     ev1 = ev2 & e1 = e2 & ve1 = ve2"
+    " v_clos(<|ev1,e1,ve1|>) = v_clos(<|ev2,e2,ve2|>) ==>
+      ev1 = ev2 & e1 = e2 & ve1 = ve2"
   
 (* All constructors are distinct *)
 
@@ -194,26 +194,26 @@
 *)
 
   eval_fun_def 
-    " eval_fun(s) == \
-\     { pp. \
-\       (? ve c. pp=<<ve,e_const(c)>,v_const(c)>) | \
-\       (? ve x. pp=<<ve,e_var(x)>,ve_app(ve,x)> & x:ve_dom(ve)) |\
-\       (? ve e x. pp=<<ve,fn x => e>,v_clos(<|x,e,ve|>)>)| \
-\       ( ? ve e x f cl. \
-\           pp=<<ve,fix f(x) = e>,v_clos(cl)> & \
-\           cl=<|x, e, ve+{f |-> v_clos(cl)} |>  \
-\       ) | \
-\       ( ? ve e1 e2 c1 c2. \
-\           pp=<<ve,e1 @ e2>,v_const(c_app(c1,c2))> & \
-\           <<ve,e1>,v_const(c1)>:s & <<ve,e2>,v_const(c2)>:s \
-\       ) | \
-\       ( ? ve vem e1 e2 em xm v v2. \
-\           pp=<<ve,e1 @ e2>,v> & \
-\           <<ve,e1>,v_clos(<|xm,em,vem|>)>:s & \
-\           <<ve,e2>,v2>:s & \
-\           <<vem+{xm |-> v2},em>,v>:s \
-\       ) \
-\     }"
+    " eval_fun(s) ==
+      { pp.
+        (? ve c. pp=<<ve,e_const(c)>,v_const(c)>) |
+        (? ve x. pp=<<ve,e_var(x)>,ve_app(ve,x)> & x:ve_dom(ve)) |
+        (? ve e x. pp=<<ve,fn x => e>,v_clos(<|x,e,ve|>)>)|
+        ( ? ve e x f cl.
+            pp=<<ve,fix f(x) = e>,v_clos(cl)> &
+            cl=<|x, e, ve+{f |-> v_clos(cl)} |> 
+        ) |
+        ( ? ve e1 e2 c1 c2.
+            pp=<<ve,e1 @ e2>,v_const(c_app(c1,c2))> &
+            <<ve,e1>,v_const(c1)>:s & <<ve,e2>,v_const(c2)>:s
+        ) |
+        ( ? ve vem e1 e2 em xm v v2.
+            pp=<<ve,e1 @ e2>,v> &
+            <<ve,e1>,v_clos(<|xm,em,vem|>)>:s &
+            <<ve,e2>,v2>:s &
+            <<vem+{xm |-> v2},em>,v>:s
+        )
+      }"
 
   eval_rel_def "eval_rel == lfp(eval_fun)"
   eval_def "ve |- e ---> v == <<ve,e>,v>:eval_rel"
@@ -224,18 +224,18 @@
 *)
 
   elab_fun_def 
-  "elab_fun(s) == \
-\  { pp. \
-\    (? te c t. pp=<<te,e_const(c)>,t> & c isof t) | \
-\    (? te x. pp=<<te,e_var(x)>,te_app(te,x)> & x:te_dom(te)) | \
-\    (? te x e t1 t2. pp=<<te,fn x => e>,t1->t2> & <<te+{x |=> t1},e>,t2>:s) | \
-\    (? te f x e t1 t2. \
-\       pp=<<te,fix f(x)=e>,t1->t2> & <<te+{f |=> t1->t2}+{x |=> t1},e>,t2>:s \
-\    ) | \
-\    (? te e1 e2 t1 t2. \
-\       pp=<<te,e1 @ e2>,t2> & <<te,e1>,t1->t2>:s & <<te,e2>,t1>:s \
-\    ) \
-\  }"
+  "elab_fun(s) ==
+   { pp.
+     (? te c t. pp=<<te,e_const(c)>,t> & c isof t) |
+     (? te x. pp=<<te,e_var(x)>,te_app(te,x)> & x:te_dom(te)) |
+     (? te x e t1 t2. pp=<<te,fn x => e>,t1->t2> & <<te+{x |=> t1},e>,t2>:s) |
+     (? te f x e t1 t2.
+        pp=<<te,fix f(x)=e>,t1->t2> & <<te+{f |=> t1->t2}+{x |=> t1},e>,t2>:s
+     ) |
+     (? te e1 e2 t1 t2.
+        pp=<<te,e1 @ e2>,t2> & <<te,e1>,t1->t2>:s & <<te,e2>,t1>:s
+     )
+   }"
 
   elab_rel_def "elab_rel == lfp(elab_fun)"
   elab_def "te |- e ===> t == <<te,e>,t>:elab_rel"
@@ -243,36 +243,36 @@
 (* The original correspondence relation *)
 
   isof_env_def 
-    " ve isofenv te == \
-\     ve_dom(ve) = te_dom(te) & \
-\     ( ! x. \
-\         x:ve_dom(ve) --> \
-\         (? c.ve_app(ve,x) = v_const(c) & c isof te_app(te,x)) \
-\     ) \
-\   "
+    " ve isofenv te ==
+      ve_dom(ve) = te_dom(te) &
+      ( ! x.
+          x:ve_dom(ve) -->
+          (? c.ve_app(ve,x) = v_const(c) & c isof te_app(te,x))
+      )
+    "
 
   isof_app "[| c1 isof t1->t2; c2 isof t1 |] ==> c_app(c1,c2) isof t2"
 
 (* The extented correspondence relation *)
 
   hasty_fun_def
-    " hasty_fun(r) == \
-\     { p. \
-\       ( ? c t. p = <v_const(c),t> & c isof t) | \
-\       ( ? ev e ve t te. \
-\           p = <v_clos(<|ev,e,ve|>),t> & \
-\           te |- fn ev => e ===> t & \
-\           ve_dom(ve) = te_dom(te) & \
-\           (! ev1.ev1:ve_dom(ve) --> <ve_app(ve,ev1),te_app(te,ev1)> : r) \
-\       ) \
-\     } \
-\   "
+    " hasty_fun(r) ==
+      { p.
+        ( ? c t. p = <v_const(c),t> & c isof t) |
+        ( ? ev e ve t te.
+            p = <v_clos(<|ev,e,ve|>),t> &
+            te |- fn ev => e ===> t &
+            ve_dom(ve) = te_dom(te) &
+            (! ev1.ev1:ve_dom(ve) --> <ve_app(ve,ev1),te_app(te,ev1)> : r)
+        )
+      }
+    "
 
   hasty_rel_def "hasty_rel == gfp(hasty_fun)"
   hasty_def "v hasty t == <v,t> : hasty_rel"
   hasty_env_def 
-    " ve hastyenv te == \
-\     ve_dom(ve) = te_dom(te) & \
-\     (! x. x: ve_dom(ve) --> ve_app(ve,x) hasty te_app(te,x))"
+    " ve hastyenv te ==
+      ve_dom(ve) = te_dom(te) &
+      (! x. x: ve_dom(ve) --> ve_app(ve,x) hasty te_app(te,x))"
 
 end