isabelle: src/FOL/ex/ROOT.ML@ab207f9c1e1e (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";
1351 4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	10	time_use "intro.ML";
4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	11	time_use_thy "Nat";
11675 c87d695f4adb theory Natural_Numbers; wenzelm parents: 9205 diff changeset	12	time_use_thy "Natural_Numbers";
1351 4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	13	time_use "foundn.ML";
4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	14	time_use_thy "Prolog";
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	15
a5a9c433f639 Initial revision clasohm parents: diff changeset	16	writeln"\n Intuitionistic examples \n";
9205 f171fa6a0989 improved arrangement of files; wenzelm parents: 9000 diff changeset	17	time_use_thy "int";
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	18
2601 b301958c465d Renamed structure Int (intuitionistic prover) to IntPr to prevent clash paulson parents: 2236 diff changeset	19	val thy = IFOL.thy and tac = IntPr.fast_tac 1;
1351 4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	20	time_use "prop.ML";
4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	21	time_use "quant.ML";
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	22
a5a9c433f639 Initial revision clasohm parents: diff changeset	23	writeln"\n Classical examples \n";
1351 4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	24	time_use "mini.ML";
4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	25	time_use "cla.ML";
4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	26	time_use_thy "If";
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	27
a5a9c433f639 Initial revision clasohm parents: diff changeset	28	val thy = FOL.thy and tac = Cla.fast_tac FOL_cs 1;
1351 4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	29	time_use "prop.ML";
4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	30	time_use "quant.ML";
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	31
8909 96503b90307b added NatClass; wenzelm parents: 6349 diff changeset	32	time_use_thy "NatClass";
96503b90307b added NatClass; wenzelm parents: 6349 diff changeset	33
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	34	writeln"\n Simplification examples \n";
1351 4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	35	time_use_thy "Nat2";
4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	36	time_use_thy "List";
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	37
1549 ac9b58304d62 Now loads IffOracle, the oracles example paulson parents: 1459 diff changeset	38	writeln"\n How to declare an oracle \n";
ac9b58304d62 Now loads IffOracle, the oracles example paulson parents: 1459 diff changeset	39	time_use_thy "IffOracle";

author	wenzelm
	Wed, 05 Dec 2001 03:05:18 +0100
changeset 12369	ab207f9c1e1e
parent 11675	c87d695f4adb
child 12393	03c55bb0ee92
permissions	-rw-r--r--