author | clasohm |
Tue, 04 Oct 1994 13:02:16 +0100 | |
changeset 624 | 33b9b5da3e6f |
parent 430 | 89e1986125fe |
child 1267 | bca91b4e1710 |
permissions | -rw-r--r-- |
(* 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 neg_thms addsimps ifte_thms;