isabelle: src/FOL/ex/ROOT.ML@53b2463ca84c (annotated)

1459 d12da312eff4 expanded tabs clasohm parents: 1351 diff changeset	1	(* Title: FOL/ex/ROOT
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
a5a9c433f639 Initial revision clasohm parents: diff changeset	6	Executes all examples for First-Order Logic.
a5a9c433f639 Initial revision clasohm parents: diff changeset	7	*)
a5a9c433f639 Initial revision clasohm parents: diff changeset	8
a5a9c433f639 Initial revision clasohm parents: diff changeset	9	writeln"Root file for FOL examples";
a5a9c433f639 Initial revision clasohm parents: diff changeset	10
1459 d12da312eff4 expanded tabs clasohm parents: 1351 diff changeset	11	FOL_build_completed; (Cause examples to fail if FOL did)
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	12
4446 097004a470fb tuned; wenzelm parents: 2601 diff changeset	13	set proof_timing;
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	14
1351 4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	15	time_use "intro.ML";
4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	16	time_use_thy "Nat";
4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	17	time_use "foundn.ML";
4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	18	time_use_thy "Prolog";
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	19
a5a9c433f639 Initial revision clasohm parents: diff changeset	20	writeln"\n Intuitionistic examples \n";
1351 4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	21	time_use "int.ML";
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	22
2601 b301958c465d Renamed structure Int (intuitionistic prover) to IntPr to prevent clash paulson parents: 2236 diff changeset	23	val thy = IFOL.thy and tac = IntPr.fast_tac 1;
1351 4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	24	time_use "prop.ML";
4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	25	time_use "quant.ML";
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	26
a5a9c433f639 Initial revision clasohm parents: diff changeset	27	writeln"\n Classical examples \n";
1351 4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	28	time_use "mini.ML";
4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	29	time_use "cla.ML";
4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	30	time_use_thy "If";
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	31
a5a9c433f639 Initial revision clasohm parents: diff changeset	32	val thy = FOL.thy and tac = Cla.fast_tac FOL_cs 1;
1351 4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	33	time_use "prop.ML";
4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	34	time_use "quant.ML";
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	35
a5a9c433f639 Initial revision clasohm parents: diff changeset	36	writeln"\n Simplification examples \n";
1351 4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	37	time_use_thy "Nat2";
4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	38	time_use_thy "List";
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	39
1549 ac9b58304d62 Now loads IffOracle, the oracles example paulson parents: 1459 diff changeset	40	writeln"\n How to declare an oracle \n";
ac9b58304d62 Now loads IffOracle, the oracles example paulson parents: 1459 diff changeset	41	time_use_thy "IffOracle";

author	wenzelm
	Thu, 05 Feb 1998 11:20:35 +0100
changeset 4603	53b2463ca84c
parent 4446	097004a470fb
child 6349	f7750d816c21
permissions	-rw-r--r--