isabelle: src/HOLCF/ROOT.ML@13d4753079fe (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
6bcb44e4d6e5 expanded tabs clasohm parents: 1361 diff changeset	4	Copyright 1993 Technische Universitaet Muenchen
243 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	ROOT file for the conservative extension of HOL by the LCF logic.
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	7	Should be executed in subdirectory HOLCF.
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	8	*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	9
5517 863f56450888 added dependance on HOL oheimb parents: 4129 diff changeset	10	HOL_build_completed; (* Cause HOLCF to fail if HOL did *)
863f56450888 added dependance on HOL oheimb parents: 4129 diff changeset	11
3623 e843c1d6f9e1 tuned; wenzelm parents: 3608 diff changeset	12	val banner = "HOLCF";
2394 91d8abf108be adaptions for symbol font oheimb parents: 2353 diff changeset	13	writeln banner;
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: 1267 diff changeset	14
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	15	print_depth 1;
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	16
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: 1267 diff changeset	17	use_thy "HOLCF";
ea0668a1c0ba added 8bit pragmas regensbu parents: 1267 diff changeset	18
4129 2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML; wenzelm parents: 4128 diff changeset	19	use "holcf_logic.ML";
2fd816aa6206 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML; wenzelm parents: 4128 diff changeset	20	use "cont_consts.ML";
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: 1267 diff changeset	21
4122 f63c283cefaf * removed "axioms" and "generated by" section oheimb parents: 4041 diff changeset	22	(* domain package *)
1285 4dd0651d692d removed incompatibility with sml regensbu parents: 1274 diff changeset	23	use "domain/library.ML";
4dd0651d692d removed incompatibility with sml regensbu parents: 1274 diff changeset	24	use "domain/syntax.ML";
4dd0651d692d removed incompatibility with sml regensbu parents: 1274 diff changeset	25	use "domain/axioms.ML";
4dd0651d692d removed incompatibility with sml regensbu parents: 1274 diff changeset	26	use "domain/theorems.ML";
4dd0651d692d removed incompatibility with sml regensbu parents: 1274 diff changeset	27	use "domain/extender.ML";
4dd0651d692d removed incompatibility with sml regensbu parents: 1274 diff changeset	28	use "domain/interface.ML";
297 5ef75ff3baeb Franz fragen nipkow parents: 243 diff changeset	29
2394 91d8abf108be adaptions for symbol font oheimb parents: 2353 diff changeset	30	print_depth 10;
91d8abf108be adaptions for symbol font oheimb parents: 2353 diff changeset	31
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1361 diff changeset	32	val HOLCF_build_completed = (); (indicate successful build)

author	paulson
	Mon, 16 Nov 1998 13:58:56 +0100
changeset 5899	13d4753079fe
parent 5517	863f56450888
child 6349	f7750d816c21
permissions	-rw-r--r--