isabelle: src/FOL/ex/ROOT.ML@ac7f67be7f1f (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	ID: $Id$
1459 d12da312eff4 expanded tabs clasohm parents: 1351 diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	4	Copyright 1992 University of Cambridge
a5a9c433f639 Initial revision clasohm parents: diff changeset	5
11675 c87d695f4adb theory Natural_Numbers; wenzelm parents: 9205 diff changeset	6	Examples for First-Order Logic.
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	7	*)
a5a9c433f639 Initial revision clasohm parents: diff changeset	8
23914 3e0424305fa4 turned ex/prop.ML, ex/quant.ML into proper theories; wenzelm parents: 23156 diff changeset	9	use_thys [
3e0424305fa4 turned ex/prop.ML, ex/quant.ML into proper theories; wenzelm parents: 23156 diff changeset	10	"First_Order_Logic",
3e0424305fa4 turned ex/prop.ML, ex/quant.ML into proper theories; wenzelm parents: 23156 diff changeset	11	"Natural_Numbers",
3e0424305fa4 turned ex/prop.ML, ex/quant.ML into proper theories; wenzelm parents: 23156 diff changeset	12	"Intro",
3e0424305fa4 turned ex/prop.ML, ex/quant.ML into proper theories; wenzelm parents: 23156 diff changeset	13	"Nat",
3e0424305fa4 turned ex/prop.ML, ex/quant.ML into proper theories; wenzelm parents: 23156 diff changeset	14	"Foundation",
3e0424305fa4 turned ex/prop.ML, ex/quant.ML into proper theories; wenzelm parents: 23156 diff changeset	15	"Prolog",
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	16
23914 3e0424305fa4 turned ex/prop.ML, ex/quant.ML into proper theories; wenzelm parents: 23156 diff changeset	17	"Intuitionistic",
3e0424305fa4 turned ex/prop.ML, ex/quant.ML into proper theories; wenzelm parents: 23156 diff changeset	18	"Propositional_Int",
3e0424305fa4 turned ex/prop.ML, ex/quant.ML into proper theories; wenzelm parents: 23156 diff changeset	19	"Quantifiers_Int",
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	20
23914 3e0424305fa4 turned ex/prop.ML, ex/quant.ML into proper theories; wenzelm parents: 23156 diff changeset	21	"Classical",
3e0424305fa4 turned ex/prop.ML, ex/quant.ML into proper theories; wenzelm parents: 23156 diff changeset	22	"Propositional_Cla",
3e0424305fa4 turned ex/prop.ML, ex/quant.ML into proper theories; wenzelm parents: 23156 diff changeset	23	"Quantifiers_Cla",
3e0424305fa4 turned ex/prop.ML, ex/quant.ML into proper theories; wenzelm parents: 23156 diff changeset	24	"Miniscope",
3e0424305fa4 turned ex/prop.ML, ex/quant.ML into proper theories; wenzelm parents: 23156 diff changeset	25	"If",
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	26
23914 3e0424305fa4 turned ex/prop.ML, ex/quant.ML into proper theories; wenzelm parents: 23156 diff changeset	27	"NatClass",
3e0424305fa4 turned ex/prop.ML, ex/quant.ML into proper theories; wenzelm parents: 23156 diff changeset	28	"IffOracle"
3e0424305fa4 turned ex/prop.ML, ex/quant.ML into proper theories; wenzelm parents: 23156 diff changeset	29	];
17277 ab45d65bf204 make LocalesTest last, because it sets funny flags; wenzelm parents: 16168 diff changeset	30
ab45d65bf204 make LocalesTest last, because it sets funny flags; wenzelm parents: 16168 diff changeset	31	(regression test for locales -- sets several global flags!)
29357 11956fa598b7 removed locale adaption layer haftmann parents: 29249 diff changeset	32	no_document use_thy "LocaleTest";
28873 2058a6b0eb20 Regression tests for new locale implementation. ballarin parents: 23914 diff changeset	33

author	wenzelm
	Sun, 11 Jan 2009 21:49:59 +0100
changeset 29450	ac7f67be7f1f
parent 29357	11956fa598b7
child 29752	ad4e3a577fd3
permissions	-rw-r--r--