isabelle: src/Pure/pure.ML@8d2372c6b5f3 (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	Locale.setup @
6313 6e4c7209ff39 HTML.setup; wenzelm parents: 6192 diff changeset	11	HTML.setup @
11761 183435fd45f2 ObjectLogic.setup; wenzelm parents: 11664 diff changeset	12	ObjectLogic.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 @
11664 eaac65411529 tuned; wenzelm parents: 11658 diff changeset	15	InductAttrib.setup @
5839 3ad1364bbb4b Isar setups; wenzelm parents: 5247 diff changeset	16	Method.setup @
6770 7eb14a4047e3 added Isar/calculation.ML; wenzelm parents: 6696 diff changeset	17	Calculation.setup @
6888 d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only); wenzelm parents: 6785 diff changeset	18	SkipProof.setup @
6653 b0b819902eaa Added setup for BrowserInfo. berghofe parents: 6366 diff changeset	19	AxClass.setup @
8965 d46b36785c70 proper token_translation for latex mode; wenzelm parents: 7718 diff changeset	20	Latex.setup @
7718 86755cc5b83c Present.setup; wenzelm parents: 6888 diff changeset	21	Present.setup @
6696 68b4f97b57cd Isamode.setup, ProofGeneral.setup; wenzelm parents: 6653 diff changeset	22	Isamode.setup @
11515 a111174ce789 Added setup for code generator. berghofe parents: 10931 diff changeset	23	ProofGeneral.setup @
12013 8d2372c6b5f3 Goals.setup; wenzelm parents: 11761 diff changeset	24	Codegen.setup @
8d2372c6b5f3 Goals.setup; wenzelm parents: 11761 diff changeset	25	Goals.setup;
5839 3ad1364bbb4b Isar setups; wenzelm parents: 5247 diff changeset	26	in
3ad1364bbb4b Isar setups; wenzelm parents: 5247 diff changeset	27	structure Pure =
3ad1364bbb4b Isar setups; wenzelm parents: 5247 diff changeset	28	struct
3ad1364bbb4b Isar setups; wenzelm parents: 5247 diff changeset	29	val thy =
10931 ef2b1dd40db9 use Sign.PureN, Sign.CPureN; wenzelm parents: 8965 diff changeset	30	PureThy.begin_theory Sign.PureN [ProtoPure.thy]
5839 3ad1364bbb4b Isar setups; wenzelm parents: 5247 diff changeset	31	\|> Theory.add_syntax Syntax.pure_appl_syntax
5905 68cdba6c178f Theory.apply replaced by Library.apply; wenzelm parents: 5863 diff changeset	32	\|> Library.apply common_setup
5839 3ad1364bbb4b Isar setups; wenzelm parents: 5247 diff changeset	33	\|> PureThy.end_theory;
3ad1364bbb4b Isar setups; wenzelm parents: 5247 diff changeset	34	end;
5092 e443bc494604 moved actual (C)Pure theories to pure.ML; wenzelm parents: diff changeset	35
5839 3ad1364bbb4b Isar setups; wenzelm parents: 5247 diff changeset	36	structure CPure =
3ad1364bbb4b Isar setups; wenzelm parents: 5247 diff changeset	37	struct
3ad1364bbb4b Isar setups; wenzelm parents: 5247 diff changeset	38	val thy =
10931 ef2b1dd40db9 use Sign.PureN, Sign.CPureN; wenzelm parents: 8965 diff changeset	39	PureThy.begin_theory Sign.CPureN [ProtoPure.thy]
5839 3ad1364bbb4b Isar setups; wenzelm parents: 5247 diff changeset	40	\|> Theory.add_syntax Syntax.pure_applC_syntax
5905 68cdba6c178f Theory.apply replaced by Library.apply; wenzelm parents: 5863 diff changeset	41	\|> Library.apply common_setup
5863 9935800edf58 Theory.copy; wenzelm parents: 5839 diff changeset	42	\|> Theory.copy
5839 3ad1364bbb4b Isar setups; wenzelm parents: 5247 diff changeset	43	\|> PureThy.end_theory;
3ad1364bbb4b Isar setups; wenzelm parents: 5247 diff changeset	44	end;
5211 c02b0c727780 late setup of Pure and CPure; wenzelm parents: 5092 diff changeset	45	end;
5092 e443bc494604 moved actual (C)Pure theories to pure.ML; wenzelm parents: diff changeset	46
6192 a42dbf1af868 proper setup of preloaded theories (ThyInfo.register_theory); wenzelm parents: 5905 diff changeset	47	ThyInfo.register_theory ProtoPure.thy;
a42dbf1af868 proper setup of preloaded theories (ThyInfo.register_theory); wenzelm parents: 5905 diff changeset	48	ThyInfo.register_theory Pure.thy;
a42dbf1af868 proper setup of preloaded theories (ThyInfo.register_theory); wenzelm parents: 5905 diff changeset	49	ThyInfo.register_theory CPure.thy;

author	wenzelm
	Thu, 01 Nov 2001 21:10:13 +0100
changeset 12013	8d2372c6b5f3
parent 11761	183435fd45f2
child 12234	9d86f1cd2969
permissions	-rw-r--r--