isabelle: doc-src/IsarRef/Thy/ROOT.ML@5b25fee0362c (annotated)

30240 5b25fee0362c Merge. blanchet parents: 28838 diff changeset	1	set quick_and_dirty;
26844 46b6306c181e enabled ThyOutput.source option by default; wenzelm parents: 26840 diff changeset	2	set ThyOutput.source;
26741 eb15fd4cd1ad converted intro.tex to Thy/intro.thy; wenzelm parents: 26738 diff changeset	3	use "../../antiquote_setup.ML";
26844 46b6306c181e enabled ThyOutput.source option by default; wenzelm parents: 26840 diff changeset	4
30240 5b25fee0362c Merge. blanchet parents: 28838 diff changeset	5	use_thys [
5b25fee0362c Merge. blanchet parents: 28838 diff changeset	6	"Introduction",
5b25fee0362c Merge. blanchet parents: 28838 diff changeset	7	"Framework",
5b25fee0362c Merge. blanchet parents: 28838 diff changeset	8	"First_Order_Logic",
5b25fee0362c Merge. blanchet parents: 28838 diff changeset	9	"Outer_Syntax",
5b25fee0362c Merge. blanchet parents: 28838 diff changeset	10	"Document_Preparation",
5b25fee0362c Merge. blanchet parents: 28838 diff changeset	11	"Spec",
5b25fee0362c Merge. blanchet parents: 28838 diff changeset	12	"Proof",
5b25fee0362c Merge. blanchet parents: 28838 diff changeset	13	"Inner_Syntax",
5b25fee0362c Merge. blanchet parents: 28838 diff changeset	14	"Misc",
5b25fee0362c Merge. blanchet parents: 28838 diff changeset	15	"Generic",
5b25fee0362c Merge. blanchet parents: 28838 diff changeset	16	"HOL_Specific",
5b25fee0362c Merge. blanchet parents: 28838 diff changeset	17	"Quick_Reference",
5b25fee0362c Merge. blanchet parents: 28838 diff changeset	18	"Symbols",
5b25fee0362c Merge. blanchet parents: 28838 diff changeset	19	"ML_Tactic"
5b25fee0362c Merge. blanchet parents: 28838 diff changeset	20	];

author	blanchet
	Wed, 04 Mar 2009 10:45:52 +0100
changeset 30240	5b25fee0362c
parent 28838	d5db6dfcb34a
child 30242	aea5d7fa7ef5
permissions	-rw-r--r--