isabelle: src/HOLCF/HOLCF.ML@23ceb1dc9755 (annotated)

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;

author	paulson
	Thu, 18 Jan 1996 10:38:29 +0100
changeset 1444	23ceb1dc9755
parent 1274	ea0668a1c0ba
child 1461	6bcb44e4d6e5
permissions	-rw-r--r--