src/HOLCF/HOLCF.ML
changeset 1267 bca91b4e1710
parent 430 89e1986125fe
child 1274 ea0668a1c0ba
--- a/src/HOLCF/HOLCF.ML	Wed Oct 04 13:12:14 1995 +0100
+++ b/src/HOLCF/HOLCF.ML	Wed Oct 04 14:01:44 1995 +0100
@@ -6,16 +6,5 @@
 
 open HOLCF;
 
-val HOLCF_ss = ccc1_ss 
-		addsimps one_when 
-		addsimps dist_less_one
-		addsimps dist_eq_one 
-		addsimps dist_less_tr
-		addsimps dist_eq_tr
-		addsimps tr_when
-		addsimps andalso_thms
-		addsimps orelse_thms
-                addsimps neg_thms
-		addsimps ifte_thms;
-
-
+Addsimps (one_when @ dist_less_one @ dist_eq_one @ dist_less_tr @ dist_eq_tr
+          @ tr_when @ andalso_thms @ orelse_thms @ neg_thms @ ifte_thms);