src/HOLCF/Sprod0.ML

 
 (* ------------------------------------------------------------------------ *)
 (* instantiate the simplifier                                               *)
 (* ------------------------------------------------------------------------ *)
 
-val Sprod_ss = 
-	HOL_ss 
-	addsimps [strict_Isfst1,strict_Isfst2,strict_Issnd1,strict_Issnd2,
-		 Isfst2,Issnd2];
+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"
  (fn prems =>

 	(cut_facts_tac prems 1),
 	(res_inst_tac [("p","p")] IsprodE 1),
 	(contr_tac 1),
 	(hyp_subst_tac 1),
 	(rtac conjI 1),
-	(asm_simp_tac Sprod_ss 1),
-	(asm_simp_tac Sprod_ss 1)
+	(Asm_simp_tac 1),
+	(Asm_simp_tac 1)
 	]);
 
 
 (* ------------------------------------------------------------------------ *)
 (* Surjective pairing: equivalent to Exh_Sprod                              *)

 qed_goal "surjective_pairing_Sprod" Sprod0.thy 
 	"z = Ispair(Isfst z)(Issnd z)"
 (fn prems =>
 	[
 	(res_inst_tac [("z1","z")] (Exh_Sprod RS disjE) 1),
-	(asm_simp_tac Sprod_ss 1),
-	(etac exE 1),
-	(etac exE 1),
-	(asm_simp_tac Sprod_ss 1)
-	]);
-
-
-
-
-
-
-
-
-
-
-
-
-
+	(Asm_simp_tac 1),
+	(etac exE 1),
+	(etac exE 1),
+	(Asm_simp_tac 1)
+	]);
+
+
+
+
+
+
+
+
+
+
+
+
+