isabelle: src/Pure/ROOT@1c75f42770b5 (annotated)

51397 03b586ee5930 support for 'chapter' specifications within session ROOT; wenzelm parents: 50911 diff changeset	1	chapter Pure
03b586ee5930 support for 'chapter' specifications within session ROOT; wenzelm parents: 50911 diff changeset	2
48738 f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default; wenzelm parents: 48732 diff changeset	3	session Pure =
69319 baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb; wenzelm parents: 69272 diff changeset	4	description "
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb; wenzelm parents: 69272 diff changeset	5	The Pure logical framework.
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb; wenzelm parents: 69272 diff changeset	6	"
70917 693e811b91bb more robust hybrid treatment of Pure, notably for Isabelle/Dedukti; wenzelm parents: 70914 diff changeset	7	options [threads = 1, export_proofs, export_standard_proofs, prune_proofs = false]
70906 b9567a9f44a0 proper export of bootstrap proofs (amending a6304b4664b6); wenzelm parents: 70905 diff changeset	8	theories [export_theory]
70905 a6304b4664b6 more robust -- avoid interference with Proofterm.proofs := 0 in ML_Bootstrap.thy; wenzelm parents: 70606 diff changeset	9	Pure (global)
62868 61a691db1c4d support for ML project ROOT file, with imitation of ML "use" commands; wenzelm parents: 62866 diff changeset	10	theories
65473 b47373f52451 more global theories; wenzelm parents: 65374 diff changeset	11	ML_Bootstrap (global)
67215 03d0c958d65a PIDE markup for session ROOT files; wenzelm parents: 65473 diff changeset	12	Sessions
71924 e5df9c8d9d4b clarified sessions: "Notable Examples in Isabelle/Pure"; wenzelm parents: 70917 diff changeset	13
e5df9c8d9d4b clarified sessions: "Notable Examples in Isabelle/Pure"; wenzelm parents: 70917 diff changeset	14	session "Pure-Examples" in Examples = Pure +
e5df9c8d9d4b clarified sessions: "Notable Examples in Isabelle/Pure"; wenzelm parents: 70917 diff changeset	15	description "
74286 641300b56ebe tuned comments; wenzelm parents: 71924 diff changeset	16	Notable Examples for Isabelle/Pure.
71924 e5df9c8d9d4b clarified sessions: "Notable Examples in Isabelle/Pure"; wenzelm parents: 70917 diff changeset	17	"
e5df9c8d9d4b clarified sessions: "Notable Examples in Isabelle/Pure"; wenzelm parents: 70917 diff changeset	18	theories
e5df9c8d9d4b clarified sessions: "Notable Examples in Isabelle/Pure"; wenzelm parents: 70917 diff changeset	19	First_Order_Logic
e5df9c8d9d4b clarified sessions: "Notable Examples in Isabelle/Pure"; wenzelm parents: 70917 diff changeset	20	Higher_Order_Logic
e5df9c8d9d4b clarified sessions: "Notable Examples in Isabelle/Pure"; wenzelm parents: 70917 diff changeset	21	document_files
e5df9c8d9d4b clarified sessions: "Notable Examples in Isabelle/Pure"; wenzelm parents: 70917 diff changeset	22	"root.bib"
e5df9c8d9d4b clarified sessions: "Notable Examples in Isabelle/Pure"; wenzelm parents: 70917 diff changeset	23	"root.tex"
74287 f79dfc7656ae miscellaneous examples and experiments for Isabelle/Pure; wenzelm parents: 74286 diff changeset	24
f79dfc7656ae miscellaneous examples and experiments for Isabelle/Pure; wenzelm parents: 74286 diff changeset	25	session "Pure-ex" in ex = Pure +
f79dfc7656ae miscellaneous examples and experiments for Isabelle/Pure; wenzelm parents: 74286 diff changeset	26	description "
f79dfc7656ae miscellaneous examples and experiments for Isabelle/Pure; wenzelm parents: 74286 diff changeset	27	Miscellaneous examples and experiments for Isabelle/Pure.
f79dfc7656ae miscellaneous examples and experiments for Isabelle/Pure; wenzelm parents: 74286 diff changeset	28	"
74836 a97ec0954c50 example: alternative document headings, based on more general document output markup; wenzelm parents: 74365 diff changeset	29	options [document_heading_prefix = ""]
74365 b49bd5d9041f improper proof command 'guess' moved to separate theory "Pure-ex.Guess"; wenzelm parents: 74287 diff changeset	30	sessions
b49bd5d9041f improper proof command 'guess' moved to separate theory "Pure-ex.Guess"; wenzelm parents: 74287 diff changeset	31	"Pure-Examples"
74836 a97ec0954c50 example: alternative document headings, based on more general document output markup; wenzelm parents: 74365 diff changeset	32	theories [document = false]
74287 f79dfc7656ae miscellaneous examples and experiments for Isabelle/Pure; wenzelm parents: 74286 diff changeset	33	Def
f79dfc7656ae miscellaneous examples and experiments for Isabelle/Pure; wenzelm parents: 74286 diff changeset	34	Def_Examples
74365 b49bd5d9041f improper proof command 'guess' moved to separate theory "Pure-ex.Guess"; wenzelm parents: 74287 diff changeset	35	Guess
b49bd5d9041f improper proof command 'guess' moved to separate theory "Pure-ex.Guess"; wenzelm parents: 74287 diff changeset	36	Guess_Examples
74836 a97ec0954c50 example: alternative document headings, based on more general document output markup; wenzelm parents: 74365 diff changeset	37	theories
a97ec0954c50 example: alternative document headings, based on more general document output markup; wenzelm parents: 74365 diff changeset	38	Alternative_Headings
a97ec0954c50 example: alternative document headings, based on more general document output markup; wenzelm parents: 74365 diff changeset	39	Alternative_Headings_Examples
a97ec0954c50 example: alternative document headings, based on more general document output markup; wenzelm parents: 74365 diff changeset	40	document_files
a97ec0954c50 example: alternative document headings, based on more general document output markup; wenzelm parents: 74365 diff changeset	41	"root.tex"

author	wenzelm
	Tue, 14 Dec 2021 09:53:54 +0100
changeset 74932	1c75f42770b5
parent 74836	a97ec0954c50
permissions	-rw-r--r--