--- a/src/HOLCF/Up1.ML Wed Jul 05 14:26:58 2000 +0200
+++ b/src/HOLCF/Up1.ML Wed Jul 05 16:37:52 2000 +0200
@@ -10,8 +10,7 @@
by (simp_tac (simpset() addsimps [Up_def,Abs_Up_inverse]) 1);
qed "Abs_Up_inverse2";
-val prems = Goalw [Iup_def ]
- "z = Abs_Up(Inl ()) | (? x. z = Iup x)";
+Goalw [Iup_def] "z = Abs_Up(Inl ()) | (? x. z = Iup x)";
by (rtac (Rep_Up_inverse RS subst) 1);
by (res_inst_tac [("s","Rep_Up z")] sumE 1);
by (rtac disjI1 1);
@@ -34,8 +33,7 @@
by (rtac Rep_Up_inverse 1);
qed "inj_Rep_Up";
-val prems = goalw thy [Iup_def] "Iup x=Iup y ==> x=y";
-by (cut_facts_tac prems 1);
+Goalw [Iup_def] "Iup x=Iup y ==> x=y";
by (rtac (inj_Inr RS injD) 1);
by (rtac (inj_Abs_Up RS injD) 1);
by (atac 1);
@@ -43,7 +41,7 @@
AddSDs [inject_Iup];
-val prems = goalw thy [Iup_def] "Iup x~=Abs_Up(Inl ())";
+Goalw [Iup_def] "Iup x~=Abs_Up(Inl ())";
by (rtac notI 1);
by (rtac notE 1);
by (rtac Inl_not_Inr 1);
@@ -59,14 +57,13 @@
by (eresolve_tac prems 1);
qed "upE";
-val prems = goalw thy [Ifup_def]
- "Ifup(f)(Abs_Up(Inl ()))=UU";
+Goalw [Ifup_def] "Ifup(f)(Abs_Up(Inl ()))=UU";
by (stac Abs_Up_inverse2 1);
by (stac sum_case_Inl 1);
by (rtac refl 1);
qed "Ifup1";
-val prems = goalw thy [Ifup_def,Iup_def]
+Goalw [Ifup_def,Iup_def]
"Ifup(f)(Iup(x))=f`x";
by (stac Abs_Up_inverse2 1);
by (stac sum_case_Inr 1);
@@ -78,14 +75,14 @@
Addsimps [Ifup1,Ifup2];
-val prems = goalw thy [less_up_def]
+Goalw [less_up_def]
"Abs_Up(Inl ())<< z";
by (stac Abs_Up_inverse2 1);
by (stac sum_case_Inl 1);
by (rtac TrueI 1);
qed "less_up1a";
-val prems = goalw thy [Iup_def,less_up_def]
+Goalw [Iup_def,less_up_def]
"~(Iup x) << (Abs_Up(Inl ()))";
by (rtac notI 1);
by (rtac iffD1 1);
@@ -97,7 +94,7 @@
by (rtac refl 1);
qed "less_up1b";
-val prems = goalw thy [Iup_def,less_up_def]
+Goalw [Iup_def,less_up_def]
"(Iup x) << (Iup y)=(x<<y)";
by (stac Abs_Up_inverse2 1);
by (stac Abs_Up_inverse2 1);