src/HOLCF/HOLCF.ML
changeset 243 c22b85994e17
child 430 89e1986125fe
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/HOLCF.ML	Wed Jan 19 17:35:01 1994 +0100
@@ -0,0 +1,20 @@
+(*  Title: 	HOLCF/HOLCF.ML
+    ID:         $Id$
+    Author: 	Franz Regensburger
+    Copyright   1993 Technische Universitaet Muenchen
+*)
+
+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 ifte_thms;
+
+