isabelle: src/ZF/AC/ROOT.ML@1f053d05f571 (annotated)

1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1351 diff changeset	1	(* Title: ZF/AC/ROOT
992 4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski lcp parents: diff changeset	2	ID: $Id$
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1351 diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
992 4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski lcp parents: diff changeset	4	Copyright 1995 University of Cambridge
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski lcp parents: diff changeset	5
1208 bc3093616ba4 Ran expandshort and corrected spelling of Grabczewski paulson parents: 1196 diff changeset	6	Executes the proofs of the AC-equivalences, due to Krzysztof Grabczewski
992 4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski lcp parents: diff changeset	7	*)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski lcp parents: diff changeset	8
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1351 diff changeset	9	ZF_build_completed; (Make examples fail if ZF did)
992 4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski lcp parents: diff changeset	10
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski lcp parents: diff changeset	11	writeln"Root file for ZF/AC";
4446 097004a470fb tuned; wenzelm parents: 1461 diff changeset	12	set proof_timing;
992 4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski lcp parents: diff changeset	13
1351 4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	14	time_use_thy "AC_Equiv";
1123 5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: 1071 diff changeset	15
1351 4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	16	time_use "WO1_WO6.ML";
4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	17	time_use_thy "WO6_WO1";
5471 a4c9eaff2333 Now WO1_WO7 has a .thy file paulson parents: 4446 diff changeset	18	time_use_thy "WO1_WO7";
1351 4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	19	time_use "WO1_WO8.ML";
1123 5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: 1071 diff changeset	20
1351 4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	21	time_use "AC0_AC1.ML";
4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	22	time_use "AC2_AC6.ML";
4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	23	time_use "AC7_AC9.ML";
992 4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski lcp parents: diff changeset	24
1351 4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	25	time_use_thy "WO1_AC";
4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	26	time_use_thy "AC1_WO2";
1123 5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: 1071 diff changeset	27
1351 4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	28	time_use "AC10_AC15.ML";
4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	29	time_use_thy "AC15_WO6";
1123 5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: 1071 diff changeset	30
1351 4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	31	time_use_thy "WO2_AC16";
4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	32	time_use_thy "AC16_WO4";
1123 5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: 1071 diff changeset	33
1351 4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	34	time_use "AC1_AC17.ML";
4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	35	time_use_thy "AC17_AC1";
1071 96dfc9977bf5 Simple updates for compatibility with KG lcp parents: 1040 diff changeset	36
1351 4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	37	time_use_thy "AC18_AC19";
1196 d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: 1123 diff changeset	38
1351 4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	39	time_use_thy "DC";
1296 ae31bb7774a7 added calls of init_html and make_chart clasohm parents: 1208 diff changeset	40
992 4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski lcp parents: diff changeset	41	writeln"END: Root file for ZF/AC";

author	wenzelm
	Tue, 20 Oct 1998 16:26:20 +0200
changeset 5686	1f053d05f571
parent 5471	a4c9eaff2333
child 6349	f7750d816c21
permissions	-rw-r--r--