isabelle: src/Pure/pure.ML@7eb14a4047e3 (annotated)

5092 e443bc494604 moved actual (C)Pure theories to pure.ML; wenzelm parents: diff changeset	1	(* Title: Pure/pure.ML
e443bc494604 moved actual (C)Pure theories to pure.ML; wenzelm parents: diff changeset	2	ID: $Id$
e443bc494604 moved actual (C)Pure theories to pure.ML; wenzelm parents: diff changeset	3	Author: Markus Wenzel, TU Muenchen
e443bc494604 moved actual (C)Pure theories to pure.ML; wenzelm parents: diff changeset	4
6192 a42dbf1af868 proper setup of preloaded theories (ThyInfo.register_theory); wenzelm parents: 5905 diff changeset	5	Final setup of the Pure theories.
5092 e443bc494604 moved actual (C)Pure theories to pure.ML; wenzelm parents: diff changeset	6	*)
e443bc494604 moved actual (C)Pure theories to pure.ML; wenzelm parents: diff changeset	7
5839 3ad1364bbb4b Isar setups; wenzelm parents: 5247 diff changeset	8	local
3ad1364bbb4b Isar setups; wenzelm parents: 5247 diff changeset	9	val common_setup =
3ad1364bbb4b Isar setups; wenzelm parents: 5247 diff changeset	10	ObjectLogic.setup @
3ad1364bbb4b Isar setups; wenzelm parents: 5247 diff changeset	11	Locale.setup @
6313 6e4c7209ff39 HTML.setup; wenzelm parents: 6192 diff changeset	12	HTML.setup @
5839 3ad1364bbb4b Isar setups; wenzelm parents: 5247 diff changeset	13	ProofContext.setup @
6770 7eb14a4047e3 added Isar/calculation.ML; wenzelm parents: 6696 diff changeset	14	Attrib.setup @
5839 3ad1364bbb4b Isar setups; wenzelm parents: 5247 diff changeset	15	Method.setup @
6770 7eb14a4047e3 added Isar/calculation.ML; wenzelm parents: 6696 diff changeset	16	Calculation.setup @
6653 b0b819902eaa Added setup for BrowserInfo. berghofe parents: 6366 diff changeset	17	AxClass.setup @
6696 68b4f97b57cd Isamode.setup, ProofGeneral.setup; wenzelm parents: 6653 diff changeset	18	BrowserInfo.setup @
68b4f97b57cd Isamode.setup, ProofGeneral.setup; wenzelm parents: 6653 diff changeset	19	Isamode.setup @
68b4f97b57cd Isamode.setup, ProofGeneral.setup; wenzelm parents: 6653 diff changeset	20	ProofGeneral.setup;
5839 3ad1364bbb4b Isar setups; wenzelm parents: 5247 diff changeset	21	in
3ad1364bbb4b Isar setups; wenzelm parents: 5247 diff changeset	22	structure Pure =
3ad1364bbb4b Isar setups; wenzelm parents: 5247 diff changeset	23	struct
3ad1364bbb4b Isar setups; wenzelm parents: 5247 diff changeset	24	val thy =
3ad1364bbb4b Isar setups; wenzelm parents: 5247 diff changeset	25	PureThy.begin_theory "Pure" [ProtoPure.thy]
3ad1364bbb4b Isar setups; wenzelm parents: 5247 diff changeset	26	\|> Theory.add_syntax Syntax.pure_appl_syntax
5905 68cdba6c178f Theory.apply replaced by Library.apply; wenzelm parents: 5863 diff changeset	27	\|> Library.apply common_setup
5839 3ad1364bbb4b Isar setups; wenzelm parents: 5247 diff changeset	28	\|> PureThy.end_theory;
3ad1364bbb4b Isar setups; wenzelm parents: 5247 diff changeset	29	end;
5092 e443bc494604 moved actual (C)Pure theories to pure.ML; wenzelm parents: diff changeset	30
5839 3ad1364bbb4b Isar setups; wenzelm parents: 5247 diff changeset	31	structure CPure =
3ad1364bbb4b Isar setups; wenzelm parents: 5247 diff changeset	32	struct
3ad1364bbb4b Isar setups; wenzelm parents: 5247 diff changeset	33	val thy =
3ad1364bbb4b Isar setups; wenzelm parents: 5247 diff changeset	34	PureThy.begin_theory "CPure" [ProtoPure.thy]
3ad1364bbb4b Isar setups; wenzelm parents: 5247 diff changeset	35	\|> Theory.add_syntax Syntax.pure_applC_syntax
5905 68cdba6c178f Theory.apply replaced by Library.apply; wenzelm parents: 5863 diff changeset	36	\|> Library.apply common_setup
5863 9935800edf58 Theory.copy; wenzelm parents: 5839 diff changeset	37	\|> Theory.copy
5839 3ad1364bbb4b Isar setups; wenzelm parents: 5247 diff changeset	38	\|> PureThy.end_theory;
3ad1364bbb4b Isar setups; wenzelm parents: 5247 diff changeset	39	end;
5211 c02b0c727780 late setup of Pure and CPure; wenzelm parents: 5092 diff changeset	40	end;
5092 e443bc494604 moved actual (C)Pure theories to pure.ML; wenzelm parents: diff changeset	41
6192 a42dbf1af868 proper setup of preloaded theories (ThyInfo.register_theory); wenzelm parents: 5905 diff changeset	42	ThyInfo.register_theory ProtoPure.thy;
a42dbf1af868 proper setup of preloaded theories (ThyInfo.register_theory); wenzelm parents: 5905 diff changeset	43	ThyInfo.register_theory Pure.thy;
a42dbf1af868 proper setup of preloaded theories (ThyInfo.register_theory); wenzelm parents: 5905 diff changeset	44	ThyInfo.register_theory CPure.thy;

author	wenzelm
	Fri, 04 Jun 1999 19:53:03 +0200
changeset 6770	7eb14a4047e3
parent 6696	68b4f97b57cd
child 6785	10b77354862b
permissions	-rw-r--r--