src/HOLCF/holcf.ML
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 243 c22b85994e17
permissions -rw-r--r--
made tutorial first;
     1 (*  Title: 	HOLCF/HOLCF.ML
     2     ID:         $Id$
     3     Author: 	Franz Regensburger
     4     Copyright   1993 Technische Universitaet Muenchen
     5 *)
     6 
     7 open HOLCF;
     8 
     9 val HOLCF_ss = ccc1_ss 
    10 		addsimps one_when 
    11 		addsimps dist_less_one
    12 		addsimps dist_eq_one 
    13 		addsimps dist_less_tr
    14 		addsimps dist_eq_tr
    15 		addsimps tr_when
    16 		addsimps andalso_thms
    17 		addsimps orelse_thms
    18 		addsimps ifte_thms;
    19 
    20