isabelle: src/FOL/ex/ROOT.ML@0ebcd575d3c6 (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!)
23914 3e0424305fa4 turned ex/prop.ML, ex/quant.ML into proper theories; wenzelm parents: 23156 diff changeset	32	no_document use_thy "LocaleTest";

author	paulson
	Fri, 05 Oct 2007 09:59:03 +0200
changeset 24854	0ebcd575d3c6
parent 23914	3e0424305fa4
child 28873	2058a6b0eb20
permissions	-rw-r--r--