isabelle: doc-src/TutorialI/ROOT.ML@0e4bb86c74fd (annotated)

48519 5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	1	Thy_Output.indent_default := 5;
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	2
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	3	use_thy "ToyList/ToyList";
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	4
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	5	use_thy "Ifexpr/Ifexpr";
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	6
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	7	use_thy "CodeGen/CodeGen";
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	8
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	9	use_thy "Trie/Trie";
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	10
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	11	use_thy "Datatype/ABexpr";
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	12	use_thy "Datatype/unfoldnested";
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	13	use_thy "Datatype/Nested";
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	14	use_thy "Datatype/Fundata";
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	15
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	16	use_thy "Fun/fun0";
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	17
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	18	use_thy "Advanced/simp2";
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	19
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	20	use_thy "CTL/PDL";
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	21	use_thy "CTL/CTL";
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	22	use_thy "CTL/CTLind";
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	23
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	24	use_thy "Inductive/Even";
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	25	use_thy "Inductive/Mutual";
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	26	use_thy "Inductive/Star";
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	27	use_thy "Inductive/AB";
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	28	use_thy "Inductive/Advanced";
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	29
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	30	use_thy "Misc/Tree";
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	31	use_thy "Misc/Tree2";
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	32	use_thy "Misc/Plus";
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	33	use_thy "Misc/case_exprs";
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	34	use_thy "Misc/fakenat";
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	35	use_thy "Misc/natsum";
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	36	use_thy "Misc/pairs";
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	37	use_thy "Misc/Option2";
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	38	use_thy "Misc/types";
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	39	use_thy "Misc/prime_def";
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	40	use_thy "Misc/simp";
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	41	use_thy "Misc/Itrev";
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	42	use_thy "Misc/AdvancedInd";
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	43	use_thy "Misc/appendix";
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	44
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	45
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	46	Thy_Output.indent_default := 0;
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	47
48521 0e4bb86c74fd adhoc reordering to prevent implicit side-effects of some theories in Types, Rules, Sets; wenzelm parents: 48519 diff changeset	48	use_thy "Protocol/NS_Public";
0e4bb86c74fd adhoc reordering to prevent implicit side-effects of some theories in Types, Rules, Sets; wenzelm parents: 48519 diff changeset	49
0e4bb86c74fd adhoc reordering to prevent implicit side-effects of some theories in Types, Rules, Sets; wenzelm parents: 48519 diff changeset	50	use_thy "Documents/Documents";
0e4bb86c74fd adhoc reordering to prevent implicit side-effects of some theories in Types, Rules, Sets; wenzelm parents: 48519 diff changeset	51
0e4bb86c74fd adhoc reordering to prevent implicit side-effects of some theories in Types, Rules, Sets; wenzelm parents: 48519 diff changeset	52	no_document use_thy "Types/Setup";
0e4bb86c74fd adhoc reordering to prevent implicit side-effects of some theories in Types, Rules, Sets; wenzelm parents: 48519 diff changeset	53	use_thy "Types/Numbers";
0e4bb86c74fd adhoc reordering to prevent implicit side-effects of some theories in Types, Rules, Sets; wenzelm parents: 48519 diff changeset	54	use_thy "Types/Pairs";
0e4bb86c74fd adhoc reordering to prevent implicit side-effects of some theories in Types, Rules, Sets; wenzelm parents: 48519 diff changeset	55	use_thy "Types/Records";
0e4bb86c74fd adhoc reordering to prevent implicit side-effects of some theories in Types, Rules, Sets; wenzelm parents: 48519 diff changeset	56	use_thy "Types/Typedefs";
0e4bb86c74fd adhoc reordering to prevent implicit side-effects of some theories in Types, Rules, Sets; wenzelm parents: 48519 diff changeset	57	use_thy "Types/Overloading";
0e4bb86c74fd adhoc reordering to prevent implicit side-effects of some theories in Types, Rules, Sets; wenzelm parents: 48519 diff changeset	58	use_thy "Types/Axioms";
0e4bb86c74fd adhoc reordering to prevent implicit side-effects of some theories in Types, Rules, Sets; wenzelm parents: 48519 diff changeset	59
48519 5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	60	use_thy "Rules/Basic";
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	61	use_thy "Rules/Blast";
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	62	use_thy "Rules/Force";
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	63	use_thy "Rules/Forward";
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	64	use_thy "Rules/Tacticals";
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	65	use_thy "Rules/find2";
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	66
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	67	use_thy "Sets/Examples";
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	68	use_thy "Sets/Functions";
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	69	use_thy "Sets/Relations";
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	70	use_thy "Sets/Recur";
5deda0549f97 simplified Tutorial sessions; wenzelm parents: diff changeset	71

author	wenzelm
	Thu, 26 Jul 2012 17:32:28 +0200
changeset 48521	0e4bb86c74fd
parent 48519	5deda0549f97
child 48524	5af593945522
permissions	-rw-r--r--