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

author	nipkow
	Fri, 07 Feb 2003 15:36:12 +0100
changeset 13808	f67a53bf63bc
parent 12036	49f6c49454c2
child 14535	7cb26928e70d
permissions	-rw-r--r--