isabelle: src/FOL/ex/ROOT.ML@d6156cb8dc2e (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";
1351 4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	11	time_use "intro.ML";
4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	12	time_use_thy "Nat";
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
14513 81d32b739a2b - Experimental command for instantiation of locales in proof contexts: ballarin parents: 14236 diff changeset	16	time_use_thy "LocaleInst";
81d32b739a2b - Experimental command for instantiation of locales in proof contexts: ballarin parents: 14236 diff changeset	17
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	18	writeln"\n Intuitionistic examples \n";
14236 c73d62ce9d1c partial conversion to Isar scripts paulson parents: 12393 diff changeset	19	time_use_thy "Intuitionistic";
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	20
2601 b301958c465d Renamed structure Int (intuitionistic prover) to IntPr to prevent clash paulson parents: 2236 diff changeset	21	val thy = IFOL.thy and tac = IntPr.fast_tac 1;
1351 4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	22	time_use "prop.ML";
4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	23	time_use "quant.ML";
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	24
a5a9c433f639 Initial revision clasohm parents: diff changeset	25	writeln"\n Classical examples \n";
1351 4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	26	time_use "mini.ML";
14236 c73d62ce9d1c partial conversion to Isar scripts paulson parents: 12393 diff changeset	27	time_use_thy "Classical";
1351 4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	28	time_use_thy "If";
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	29
a5a9c433f639 Initial revision clasohm parents: diff changeset	30	val thy = FOL.thy and tac = Cla.fast_tac FOL_cs 1;
1351 4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	31	time_use "prop.ML";
4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	32	time_use "quant.ML";
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	33
8909 96503b90307b added NatClass; wenzelm parents: 6349 diff changeset	34	time_use_thy "NatClass";
96503b90307b added NatClass; wenzelm parents: 6349 diff changeset	35
0 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	kleing
	Sat, 30 Apr 2005 14:18:36 +0200
changeset 15900	d6156cb8dc2e
parent 14513	81d32b739a2b
child 16168	adb83939177f
permissions	-rw-r--r--