isabelle: src/Pure/pure.ML@2955ee2424ce (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 @
5839 3ad1364bbb4b Isar setups; wenzelm parents: 5247 diff changeset	12	ProofContext.setup @
6770 7eb14a4047e3 added Isar/calculation.ML; wenzelm parents: 6696 diff changeset	13	Attrib.setup @
5839 3ad1364bbb4b Isar setups; wenzelm parents: 5247 diff changeset	14	Method.setup @
6770 7eb14a4047e3 added Isar/calculation.ML; wenzelm parents: 6696 diff changeset	15	Calculation.setup @
6888 d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only); wenzelm parents: 6785 diff changeset	16	SkipProof.setup @
6653 b0b819902eaa Added setup for BrowserInfo. berghofe parents: 6366 diff changeset	17	AxClass.setup @
8965 d46b36785c70 proper token_translation for latex mode; wenzelm parents: 7718 diff changeset	18	Latex.setup @
7718 86755cc5b83c Present.setup; wenzelm parents: 6888 diff changeset	19	Present.setup @
6696 68b4f97b57cd Isamode.setup, ProofGeneral.setup; wenzelm parents: 6653 diff changeset	20	Isamode.setup @
68b4f97b57cd Isamode.setup, ProofGeneral.setup; wenzelm parents: 6653 diff changeset	21	ProofGeneral.setup;
5839 3ad1364bbb4b Isar setups; wenzelm parents: 5247 diff changeset	22	in
3ad1364bbb4b Isar setups; wenzelm parents: 5247 diff changeset	23	structure Pure =
3ad1364bbb4b Isar setups; wenzelm parents: 5247 diff changeset	24	struct
3ad1364bbb4b Isar setups; wenzelm parents: 5247 diff changeset	25	val thy =
3ad1364bbb4b Isar setups; wenzelm parents: 5247 diff changeset	26	PureThy.begin_theory "Pure" [ProtoPure.thy]
3ad1364bbb4b Isar setups; wenzelm parents: 5247 diff changeset	27	\|> Theory.add_syntax Syntax.pure_appl_syntax
5905 68cdba6c178f Theory.apply replaced by Library.apply; wenzelm parents: 5863 diff changeset	28	\|> Library.apply common_setup
5839 3ad1364bbb4b Isar setups; wenzelm parents: 5247 diff changeset	29	\|> PureThy.end_theory;
3ad1364bbb4b Isar setups; wenzelm parents: 5247 diff changeset	30	end;
5092 e443bc494604 moved actual (C)Pure theories to pure.ML; wenzelm parents: diff changeset	31
5839 3ad1364bbb4b Isar setups; wenzelm parents: 5247 diff changeset	32	structure CPure =
3ad1364bbb4b Isar setups; wenzelm parents: 5247 diff changeset	33	struct
3ad1364bbb4b Isar setups; wenzelm parents: 5247 diff changeset	34	val thy =
3ad1364bbb4b Isar setups; wenzelm parents: 5247 diff changeset	35	PureThy.begin_theory "CPure" [ProtoPure.thy]
3ad1364bbb4b Isar setups; wenzelm parents: 5247 diff changeset	36	\|> Theory.add_syntax Syntax.pure_applC_syntax
5905 68cdba6c178f Theory.apply replaced by Library.apply; wenzelm parents: 5863 diff changeset	37	\|> Library.apply common_setup
5863 9935800edf58 Theory.copy; wenzelm parents: 5839 diff changeset	38	\|> Theory.copy
5839 3ad1364bbb4b Isar setups; wenzelm parents: 5247 diff changeset	39	\|> PureThy.end_theory;
3ad1364bbb4b Isar setups; wenzelm parents: 5247 diff changeset	40	end;
5211 c02b0c727780 late setup of Pure and CPure; wenzelm parents: 5092 diff changeset	41	end;
5092 e443bc494604 moved actual (C)Pure theories to pure.ML; wenzelm parents: diff changeset	42
6192 a42dbf1af868 proper setup of preloaded theories (ThyInfo.register_theory); wenzelm parents: 5905 diff changeset	43	ThyInfo.register_theory ProtoPure.thy;
a42dbf1af868 proper setup of preloaded theories (ThyInfo.register_theory); wenzelm parents: 5905 diff changeset	44	ThyInfo.register_theory Pure.thy;
a42dbf1af868 proper setup of preloaded theories (ThyInfo.register_theory); wenzelm parents: 5905 diff changeset	45	ThyInfo.register_theory CPure.thy;

author	wenzelm
	Mon, 06 Nov 2000 22:50:01 +0100
changeset 10403	2955ee2424ce
parent 8965	d46b36785c70
child 10931	ef2b1dd40db9
permissions	-rw-r--r--