isabelle: src/FOLP/ex/ROOT.ML@c20d58286a51 (annotated)

1459 d12da312eff4 expanded tabs clasohm parents: 1351 diff changeset	1	(* Title: FOLP/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
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";
4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	11	time_use "foundn.ML";
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	12
a5a9c433f639 Initial revision clasohm parents: diff changeset	13	writeln"\n Intuitionistic examples \n";
1351 4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	14	time_use "int.ML";
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	15
2603 4988dda71c0b Renamed structure Int (intuitionistic prover) to IntPr to prevent clash paulson parents: 2236 diff changeset	16	val thy = IFOLP.thy and tac = IntPr.fast_tac 1;
1351 4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	17	time_use "prop.ML";
4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	18	time_use "quant.ML";
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	19
a5a9c433f639 Initial revision clasohm parents: diff changeset	20	writeln"\n Classical examples \n";
1351 4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	21	time_use "cla.ML";
4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	22	time_use_thy "If";
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	23
a5a9c433f639 Initial revision clasohm parents: diff changeset	24	val thy = FOLP.thy and tac = Cla.fast_tac FOLP_cs 1;
1351 4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	25	time_use "prop.ML";
4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	26	time_use "quant.ML";

author	wenzelm
	Tue, 30 May 2000 16:08:38 +0200
changeset 9000	c20d58286a51
parent 6349	f7750d816c21
child 17480	fd19f77dcf60
permissions	-rw-r--r--