src/HOLCF/HOLCF.ML
author regensbu
Fri, 06 Oct 1995 17:25:24 +0100
changeset 1274 ea0668a1c0ba
parent 1267 bca91b4e1710
child 1461 6bcb44e4d6e5
permissions -rw-r--r--
added 8bit pragmas added directory ax_ops for sections axioms and ops added directory domain for sections domain and generated this is the type definition package of David Oheimb
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     1
(*  Title: 	HOLCF/HOLCF.ML
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     2
    ID:         $Id$
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     3
    Author: 	Franz Regensburger
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     4
    Copyright   1993 Technische Universitaet Muenchen
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     5
*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     6
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     7
open HOLCF;
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     8
1267
bca91b4e1710 added local simpsets
clasohm
parents: 430
diff changeset
     9
Addsimps (one_when @ dist_less_one @ dist_eq_one @ dist_less_tr @ dist_eq_tr
bca91b4e1710 added local simpsets
clasohm
parents: 430
diff changeset
    10
          @ tr_when @ andalso_thms @ orelse_thms @ neg_thms @ ifte_thms);
1274
ea0668a1c0ba added 8bit pragmas
regensbu
parents: 1267
diff changeset
    11
ea0668a1c0ba added 8bit pragmas
regensbu
parents: 1267
diff changeset
    12
val HOLCF_ss = !simpset;