isabelle: src/FOL/ex/ROOT.ML@c87d695f4adb (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
1351 4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	9	time_use "intro.ML";
4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	10	time_use_thy "Nat";
11675 c87d695f4adb theory Natural_Numbers; wenzelm parents: 9205 diff changeset	11	time_use_thy "Natural_Numbers";
1351 4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	12	time_use "foundn.ML";
4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	13	time_use_thy "Prolog";
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	14
a5a9c433f639 Initial revision clasohm parents: diff changeset	15	writeln"\n Intuitionistic examples \n";
9205 f171fa6a0989 improved arrangement of files; wenzelm parents: 9000 diff changeset	16	time_use_thy "int";
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";
1351 4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	23	time_use "mini.ML";
4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	24	time_use "cla.ML";
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
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	33	writeln"\n Simplification examples \n";
1351 4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	34	time_use_thy "Nat2";
4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	35	time_use_thy "List";
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	36
1549 ac9b58304d62 Now loads IffOracle, the oracles example paulson parents: 1459 diff changeset	37	writeln"\n How to declare an oracle \n";
ac9b58304d62 Now loads IffOracle, the oracles example paulson parents: 1459 diff changeset	38	time_use_thy "IffOracle";

author	wenzelm
	Thu, 04 Oct 2001 15:26:14 +0200
changeset 11675	c87d695f4adb
parent 9205	f171fa6a0989
child 12369	ab207f9c1e1e
permissions	-rw-r--r--