isabelle: src/FOL/ex/ROOT.ML@470fd769ae53 (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!)
37134 29bd6c2ffba8 Revise locale test theory layout. ballarin parents: 29752 diff changeset	26	no_document use_thy "Locale_Test/Locale_Test";

author	wenzelm
	Thu, 02 Sep 2010 23:26:21 +0200
changeset 39042	470fd769ae53
parent 37134	29bd6c2ffba8
child 40239	c4336e45f199
permissions	-rw-r--r--