isabelle: src/HOLCF/ROOT.ML@0024472afce7 (annotated)

3623 e843c1d6f9e1 tuned; wenzelm parents: 3608 diff changeset	1	(* Title: HOLCF/ROOT.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: 1361 diff changeset	3	Author: Franz Regensburger
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	4
12036 49f6c49454c2 GPLed; wenzelm parents: 6349 diff changeset	5	Conservative (semantic) extension of HOL by the LCF logic.
243 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
3623 e843c1d6f9e1 tuned; wenzelm parents: 3608 diff changeset	8	val banner = "HOLCF";
2394 91d8abf108be adaptions for symbol font oheimb parents: 2353 diff changeset	9	writeln banner;
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: 1267 diff changeset	10
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	11	print_depth 1;
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	12
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: 1267 diff changeset	13	use_thy "HOLCF";
ea0668a1c0ba added 8bit pragmas regensbu parents: 1267 diff changeset	14
4129 2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML; wenzelm parents: 4128 diff changeset	15	use "holcf_logic.ML";
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML; wenzelm parents: 4128 diff changeset	16	use "cont_consts.ML";
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: 1267 diff changeset	17
4122 f63c283cefaf * removed "axioms" and "generated by" section oheimb parents: 4041 diff changeset	18	(* domain package *)
1285 4dd0651d692d removed incompatibility with sml regensbu parents: 1274 diff changeset	19	use "domain/library.ML";
4dd0651d692d removed incompatibility with sml regensbu parents: 1274 diff changeset	20	use "domain/syntax.ML";
4dd0651d692d removed incompatibility with sml regensbu parents: 1274 diff changeset	21	use "domain/axioms.ML";
4dd0651d692d removed incompatibility with sml regensbu parents: 1274 diff changeset	22	use "domain/theorems.ML";
4dd0651d692d removed incompatibility with sml regensbu parents: 1274 diff changeset	23	use "domain/extender.ML";
4dd0651d692d removed incompatibility with sml regensbu parents: 1274 diff changeset	24	use "domain/interface.ML";
297 5ef75ff3baeb Franz fragen nipkow parents: 243 diff changeset	25
14535 7cb26928e70d added Streams.thy (with stream concatenation etc.) oheimb parents: 12036 diff changeset	26	path_add "~~/src/HOLCF/ex";
7cb26928e70d added Streams.thy (with stream concatenation etc.) oheimb parents: 12036 diff changeset	27
2394 91d8abf108be adaptions for symbol font oheimb parents: 2353 diff changeset	28	print_depth 10;

author	nipkow
	Tue, 22 Feb 2005 10:54:30 +0100
changeset 15543	0024472afce7
parent 15188	9d57263faf9e
child 16483	ace3c2b95353
permissions	-rw-r--r--