isabelle: src/HOLCF/HOLCF.ML@9acc10ac1e1d (annotated)

1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1274 diff changeset	1	(* Title: HOLCF/HOLCF.ML
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	2	ID: $Id$
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1274 diff changeset	3	Author: Franz Regensburger
243 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
	Wed, 25 Sep 1996 15:03:13 +0200
changeset 2025	9acc10ac1e1d
parent 1461	6bcb44e4d6e5
child 2355	ee9bdbe2ac8a
permissions	-rw-r--r--