src/HOLCF/Cprod1.ML

--- a/src/HOLCF/Cprod1.ML	Wed Jul 05 14:26:58 2000 +0200
+++ b/src/HOLCF/Cprod1.ML	Wed Jul 05 16:37:52 2000 +0200
@@ -11,16 +11,14 @@
 (* less_cprod is a partial order on 'a * 'b                                 *)
 (* ------------------------------------------------------------------------ *)
 
-val prems = goal Prod.thy
-        "[|fst x = fst y; snd x = snd y|] ==> x = y";
-by (cut_facts_tac prems 1);
+Goal "[|fst x = fst y; snd x = snd y|] ==> x = y";
 by (subgoal_tac "(fst x,snd x)=(fst y,snd y)" 1);
 by (rotate_tac ~1 1);
 by (asm_full_simp_tac(HOL_ss addsimps[surjective_pairing RS sym])1);
 by (asm_simp_tac (simpset_of Prod.thy) 1);
 qed "Sel_injective_cprod";
 
-val prems = goalw Cprod1.thy [less_cprod_def] "(p::'a*'b) << p";
+Goalw [less_cprod_def] "(p::'a*'b) << p";
 by (Simp_tac 1);
 qed "refl_less_cprod";
 
@@ -30,9 +28,8 @@
 by (fast_tac (HOL_cs addIs [antisym_less]) 1);
 qed "antisym_less_cprod";
 
-val prems = goalw thy [less_cprod_def]
+Goalw [less_cprod_def]
         "[|(p1::'a*'b) << p2;p2 << p3|] ==> p1 << p3";
-by (cut_facts_tac prems 1);
 by (rtac conjI 1);
 by (fast_tac (HOL_cs addIs [trans_less]) 1);
 by (fast_tac (HOL_cs addIs [trans_less]) 1);