isabelle: src/Pure/pure.ML@22d4c641ebff (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 @
7718 86755cc5b83c Present.setup; wenzelm parents: 6888 diff changeset	18	Present.setup @
6696 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	paulson
	Sun, 23 Apr 2000 11:33:41 +0200
changeset 8763	22d4c641ebff
parent 7718	86755cc5b83c
child 8965	d46b36785c70
permissions	-rw-r--r--