src/HOLCF/Lift3.ML

--- a/src/HOLCF/Lift3.ML	Mon Jun 22 17:12:27 1998 +0200
+++ b/src/HOLCF/Lift3.ML	Mon Jun 22 17:13:09 1998 +0200
@@ -70,7 +70,7 @@
               section"less_lift";
 (* --------------------------------------------------------*)
 
-goal thy "(x::'a lift) << y = (x=y | x=UU)";
+Goal "(x::'a lift) << y = (x=y | x=UU)";
 by (stac inst_lift_po 1);
 by (Simp_tac 1);
 qed"less_lift";
@@ -80,7 +80,7 @@
                  section"UU and Def";             
 (* ---------------------------------------------------------- *)
 
-goal thy "x=UU | (? y. x=Def y)"; 
+Goal "x=UU | (? y. x=Def y)"; 
 by (lift.induct_tac "x" 1);
 by (Asm_simp_tac 1);
 by (rtac disjI2 1);
@@ -94,7 +94,7 @@
 by (fast_tac (HOL_cs addSEs prems) 1);
 qed"Lift_cases";
 
-goal thy "(x~=UU)=(? y. x=Def y)";
+Goal "(x~=UU)=(? y. x=Def y)";
 by (rtac iffI 1);
 by (rtac Lift_cases 1);
 by (REPEAT (fast_tac (HOL_cs addSIs lift.distinct) 1));
@@ -115,7 +115,7 @@
 by (fast_tac (HOL_cs addSDs [DefE]) 1);
 qed"DefE2";
 
-goal thy "Def x << Def y = (x = y)";
+Goal "Def x << Def y = (x = y)";
 by (stac (hd lift.inject RS sym) 1);
 back();
 by (rtac iffI 1);
@@ -123,7 +123,7 @@
 by (etac (antisym_less_inverse RS conjunct1) 1);
 qed"Def_inject_less_eq";
 
-goal thy "Def x << y = (Def x = y)";
+Goal "Def x << y = (Def x = y)";
 by (simp_tac (simpset() addsimps [less_lift]) 1);
 qed"Def_less_is_eq";
 
@@ -133,19 +133,19 @@
               section"Lift is flat";
 (* ---------------------------------------------------------- *)
 
-goal thy "! x y::'a lift. x << y --> x = UU | x = y";
+Goal "! x y::'a lift. x << y --> x = UU | x = y";
 by (simp_tac (simpset() addsimps [less_lift]) 1);
 qed"ax_flat_lift";
 
 (* Two specific lemmas for the combination of LCF and HOL terms *)
 
-goal thy "!!f.[|cont g; cont f|] ==> cont(%x. ((f x)`(g x)) s)";
+Goal "!!f.[|cont g; cont f|] ==> cont(%x. ((f x)`(g x)) s)";
 by (rtac cont2cont_CF1L 1);
 by (REPEAT (resolve_tac cont_lemmas1 1));
 by Auto_tac;
 qed"cont_fapp_app";
 
-goal thy "!!f.[|cont g; cont f|] ==> cont(%x. ((f x)`(g x)) s t)";
+Goal "!!f.[|cont g; cont f|] ==> cont(%x. ((f x)`(g x)) s t)";
 by (rtac cont2cont_CF1L 1);
 by (etac cont_fapp_app 1);
 by (assume_tac 1);