isabelle: doc-src/IsarRef/Thy/ROOT.ML@9ece73262746 (annotated)

38767 d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar; wenzelm parents: 37216 diff changeset	1	quick_and_dirty := true;
26844 46b6306c181e enabled ThyOutput.source option by default; wenzelm parents: 26840 diff changeset	2
30167 faf7b2ba1fef simultaneous use_thys; wenzelm parents: 29730 diff changeset	3	use_thys [
42915 f35aae36cad0 turned "Overview" into "Preface" (similar to doc-src/Intro/intro.tex); wenzelm parents: 42651 diff changeset	4	"Preface",
42917 ba23e83b0868 added Synopsis, with some "Notepad" material; wenzelm parents: 42915 diff changeset	5	"Synopsis",
30167 faf7b2ba1fef simultaneous use_thys; wenzelm parents: 29730 diff changeset	6	"Framework",
faf7b2ba1fef simultaneous use_thys; wenzelm parents: 29730 diff changeset	7	"First_Order_Logic",
faf7b2ba1fef simultaneous use_thys; wenzelm parents: 29730 diff changeset	8	"Outer_Syntax",
faf7b2ba1fef simultaneous use_thys; wenzelm parents: 29730 diff changeset	9	"Document_Preparation",
faf7b2ba1fef simultaneous use_thys; wenzelm parents: 29730 diff changeset	10	"Spec",
faf7b2ba1fef simultaneous use_thys; wenzelm parents: 29730 diff changeset	11	"Proof",
faf7b2ba1fef simultaneous use_thys; wenzelm parents: 29730 diff changeset	12	"Inner_Syntax",
faf7b2ba1fef simultaneous use_thys; wenzelm parents: 29730 diff changeset	13	"Misc",
faf7b2ba1fef simultaneous use_thys; wenzelm parents: 29730 diff changeset	14	"Generic",
faf7b2ba1fef simultaneous use_thys; wenzelm parents: 29730 diff changeset	15	"HOL_Specific",
faf7b2ba1fef simultaneous use_thys; wenzelm parents: 29730 diff changeset	16	"Quick_Reference",
faf7b2ba1fef simultaneous use_thys; wenzelm parents: 29730 diff changeset	17	"Symbols",
faf7b2ba1fef simultaneous use_thys; wenzelm parents: 29730 diff changeset	18	"ML_Tactic"
faf7b2ba1fef simultaneous use_thys; wenzelm parents: 29730 diff changeset	19	];

author	bulwahn
	Sun, 03 Jul 2011 09:59:25 +0200
changeset 43656	9ece73262746
parent 42917	ba23e83b0868
permissions	-rw-r--r--