isabelle: src/HOLCF/ROOT.ML@c12c2f411f77 (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
ea0668a1c0ba added 8bit pragmas regensbu parents: 1267 diff changeset	11	use_thy "HOLCF";
ea0668a1c0ba added 8bit pragmas regensbu parents: 1267 diff changeset	12
4129 2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML; wenzelm parents: 4128 diff changeset	13	use "holcf_logic.ML";
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML; wenzelm parents: 4128 diff changeset	14	use "cont_consts.ML";
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: 1267 diff changeset	15
4122 f63c283cefaf * removed "axioms" and "generated by" section oheimb parents: 4041 diff changeset	16	(* domain package *)
1285 4dd0651d692d removed incompatibility with sml regensbu parents: 1274 diff changeset	17	use "domain/library.ML";
4dd0651d692d removed incompatibility with sml regensbu parents: 1274 diff changeset	18	use "domain/syntax.ML";
4dd0651d692d removed incompatibility with sml regensbu parents: 1274 diff changeset	19	use "domain/axioms.ML";
4dd0651d692d removed incompatibility with sml regensbu parents: 1274 diff changeset	20	use "domain/theorems.ML";
4dd0651d692d removed incompatibility with sml regensbu parents: 1274 diff changeset	21	use "domain/extender.ML";
4dd0651d692d removed incompatibility with sml regensbu parents: 1274 diff changeset	22	use "domain/interface.ML";
297 5ef75ff3baeb Franz fragen nipkow parents: 243 diff changeset	23
14535 7cb26928e70d added Streams.thy (with stream concatenation etc.) oheimb parents: 12036 diff changeset	24	path_add "~~/src/HOLCF/ex";

author	wenzelm
	Fri, 01 Jul 2005 14:41:57 +0200
changeset 16653	c12c2f411f77
parent 16483	ace3c2b95353
child 16841	228d663cc9b3
permissions	-rw-r--r--