isabelle: src/FOL/ex/ROOT.ML@2ed1b971fc20 (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",
40239 c4336e45f199 moved FOL/ex/Iff_Oracle.thy to HOL/ex where it is more accessible to most readers of isar-ref; wenzelm parents: 37134 diff changeset	21	"If"
23914 3e0424305fa4 turned ex/prop.ML, ex/quant.ML into proper theories; wenzelm parents: 23156 diff changeset	22	];
17277 ab45d65bf204 make LocalesTest last, because it sets funny flags; wenzelm parents: 16168 diff changeset	23
ab45d65bf204 make LocalesTest last, because it sets funny flags; wenzelm parents: 16168 diff changeset	24	(regression test for locales -- sets several global flags!)
37134 29bd6c2ffba8 Revise locale test theory layout. ballarin parents: 29752 diff changeset	25	no_document use_thy "Locale_Test/Locale_Test";

author	blanchet
	Tue, 07 Dec 2010 11:56:01 +0100
changeset 41051	2ed1b971fc20
parent 40239	c4336e45f199
child 41306	95449e4b4bf6
permissions	-rw-r--r--