--- a/src/HOLCF/Sprod0.ML Mon Oct 09 14:57:55 1995 +0100
+++ b/src/HOLCF/Sprod0.ML Tue Oct 10 11:55:45 1995 +0100
@@ -340,8 +340,10 @@
(* instantiate the simplifier *)
(* ------------------------------------------------------------------------ *)
-Addsimps [strict_Isfst1,strict_Isfst2,strict_Issnd1,strict_Issnd2,
- Isfst2,Issnd2];
+val Sprod0_ss =
+ HOL_ss
+ addsimps [strict_Isfst1,strict_Isfst2,strict_Issnd1,strict_Issnd2,
+ Isfst2,Issnd2];
qed_goal "defined_IsfstIssnd" Sprod0.thy
"p~=Ispair UU UU ==> Isfst p ~= UU & Issnd p ~= UU"
@@ -352,8 +354,8 @@
(contr_tac 1),
(hyp_subst_tac 1),
(rtac conjI 1),
- (Asm_simp_tac 1),
- (Asm_simp_tac 1)
+ (asm_simp_tac Sprod0_ss 1),
+ (asm_simp_tac Sprod0_ss 1)
]);
@@ -366,21 +368,9 @@
(fn prems =>
[
(res_inst_tac [("z1","z")] (Exh_Sprod RS disjE) 1),
- (Asm_simp_tac 1),
+ (asm_simp_tac Sprod0_ss 1),
(etac exE 1),
(etac exE 1),
- (Asm_simp_tac 1)
+ (asm_simp_tac Sprod0_ss 1)
]);
-
-
-
-
-
-
-
-
-
-
-
-