isabelle: src/FOL/ex/ROOT.ML@e795b5a031af (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
12369 ab207f9c1e1e added First_Order_Logic.thy; wenzelm parents: 11675 diff changeset	9	time_use_thy "First_Order_Logic";
12393 03c55bb0ee92 tuned; wenzelm parents: 12369 diff changeset	10	time_use_thy "Natural_Numbers";
19819 14de4d05d275 removed obsolete ML files; wenzelm parents: 17277 diff changeset	11	time_use_thy "Intro";
1351 4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	12	time_use_thy "Nat";
19819 14de4d05d275 removed obsolete ML files; wenzelm parents: 17277 diff changeset	13	time_use_thy "Foundation";
1351 4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	14	time_use_thy "Prolog";
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	15
14236 c73d62ce9d1c partial conversion to Isar scripts paulson parents: 12393 diff changeset	16	time_use_thy "Intuitionistic";
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	17
2601 b301958c465d Renamed structure Int (intuitionistic prover) to IntPr to prevent clash paulson parents: 2236 diff changeset	18	val thy = IFOL.thy and tac = IntPr.fast_tac 1;
1351 4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	19	time_use "prop.ML";
4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	20	time_use "quant.ML";
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	21
a5a9c433f639 Initial revision clasohm parents: diff changeset	22	writeln"\n Classical examples \n";
19820 0d7564c798d0 removed obsolete ML files; wenzelm parents: 19819 diff changeset	23	time_use_thy "Miniscope";
14236 c73d62ce9d1c partial conversion to Isar scripts paulson parents: 12393 diff changeset	24	time_use_thy "Classical";
1351 4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	25	time_use_thy "If";
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	26
a5a9c433f639 Initial revision clasohm parents: diff changeset	27	val thy = FOL.thy and tac = Cla.fast_tac FOL_cs 1;
1351 4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	28	time_use "prop.ML";
4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	29	time_use "quant.ML";
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	30
8909 96503b90307b added NatClass; wenzelm parents: 6349 diff changeset	31	time_use_thy "NatClass";
96503b90307b added NatClass; wenzelm parents: 6349 diff changeset	32
1549 ac9b58304d62 Now loads IffOracle, the oracles example paulson parents: 1459 diff changeset	33	time_use_thy "IffOracle";
17277 ab45d65bf204 make LocalesTest last, because it sets funny flags; wenzelm parents: 16168 diff changeset	34
ab45d65bf204 make LocalesTest last, because it sets funny flags; wenzelm parents: 16168 diff changeset	35	(regression test for locales -- sets several global flags!)
ab45d65bf204 make LocalesTest last, because it sets funny flags; wenzelm parents: 16168 diff changeset	36	time_use_thy "LocaleTest";

author	haftmann
	Mon, 07 May 2007 14:20:32 +0200
changeset 22850	e795b5a031af
parent 22822	c1a6a2159e69
child 23156	6ec9e29143e9
permissions	-rw-r--r--