isabelle: src/FOL/ex/ROOT.ML@ad4e3a577fd3 (annotated)

11675 c87d695f4adb theory Natural_Numbers; wenzelm parents: 9205 diff changeset	1	(* Title: FOL/ex/ROOT.ML
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	2
11675 c87d695f4adb theory Natural_Numbers; wenzelm parents: 9205 diff changeset	3	Examples for First-Order Logic.
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	4	*)
a5a9c433f639 Initial revision clasohm parents: diff changeset	5
23914 3e0424305fa4 turned ex/prop.ML, ex/quant.ML into proper theories; wenzelm parents: 23156 diff changeset	6	use_thys [
3e0424305fa4 turned ex/prop.ML, ex/quant.ML into proper theories; wenzelm parents: 23156 diff changeset	7	"First_Order_Logic",
3e0424305fa4 turned ex/prop.ML, ex/quant.ML into proper theories; wenzelm parents: 23156 diff changeset	8	"Natural_Numbers",
3e0424305fa4 turned ex/prop.ML, ex/quant.ML into proper theories; wenzelm parents: 23156 diff changeset	9	"Intro",
3e0424305fa4 turned ex/prop.ML, ex/quant.ML into proper theories; wenzelm parents: 23156 diff changeset	10	"Nat",
29752 ad4e3a577fd3 modernized some theory names; wenzelm parents: 29357 diff changeset	11	"Nat_Class",
23914 3e0424305fa4 turned ex/prop.ML, ex/quant.ML into proper theories; wenzelm parents: 23156 diff changeset	12	"Foundation",
3e0424305fa4 turned ex/prop.ML, ex/quant.ML into proper theories; wenzelm parents: 23156 diff changeset	13	"Prolog",
3e0424305fa4 turned ex/prop.ML, ex/quant.ML into proper theories; wenzelm parents: 23156 diff changeset	14	"Intuitionistic",
3e0424305fa4 turned ex/prop.ML, ex/quant.ML into proper theories; wenzelm parents: 23156 diff changeset	15	"Propositional_Int",
3e0424305fa4 turned ex/prop.ML, ex/quant.ML into proper theories; wenzelm parents: 23156 diff changeset	16	"Quantifiers_Int",
3e0424305fa4 turned ex/prop.ML, ex/quant.ML into proper theories; wenzelm parents: 23156 diff changeset	17	"Classical",
3e0424305fa4 turned ex/prop.ML, ex/quant.ML into proper theories; wenzelm parents: 23156 diff changeset	18	"Propositional_Cla",
3e0424305fa4 turned ex/prop.ML, ex/quant.ML into proper theories; wenzelm parents: 23156 diff changeset	19	"Quantifiers_Cla",
3e0424305fa4 turned ex/prop.ML, ex/quant.ML into proper theories; wenzelm parents: 23156 diff changeset	20	"Miniscope",
3e0424305fa4 turned ex/prop.ML, ex/quant.ML into proper theories; wenzelm parents: 23156 diff changeset	21	"If",
29752 ad4e3a577fd3 modernized some theory names; wenzelm parents: 29357 diff changeset	22	"Iff_Oracle"
23914 3e0424305fa4 turned ex/prop.ML, ex/quant.ML into proper theories; wenzelm parents: 23156 diff changeset	23	];
17277 ab45d65bf204 make LocalesTest last, because it sets funny flags; wenzelm parents: 16168 diff changeset	24
ab45d65bf204 make LocalesTest last, because it sets funny flags; wenzelm parents: 16168 diff changeset	25	(regression test for locales -- sets several global flags!)
29357 11956fa598b7 removed locale adaption layer haftmann parents: 29249 diff changeset	26	no_document use_thy "LocaleTest";

author	wenzelm
	Mon, 16 Feb 2009 20:15:40 +0100
changeset 29752	ad4e3a577fd3
parent 29357	11956fa598b7
child 37134	29bd6c2ffba8
permissions	-rw-r--r--