isabelle: src/ZF/ROOT.ML@bb6db6c0d4df (annotated)

12175 5cf58a1799a7 rearranged inductive package for Isar; wenzelm parents: 12133 diff changeset	1	(* Title: ZF/ROOT.ML
6 8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not lcp parents: 5 diff changeset	2	ID: $Id$
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1361 diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	4	Copyright 1993 University of Cambridge
a5a9c433f639 Initial revision clasohm parents: diff changeset	5
12175 5cf58a1799a7 rearranged inductive package for Isar; wenzelm parents: 12133 diff changeset	6	Zermelo-Fraenkel Set Theory on top of classical First-Order Logic.
5cf58a1799a7 rearranged inductive package for Isar; wenzelm parents: 12133 diff changeset	7	This theory is the work of Martin Coen, Philippe Noel and Lawrence
5cf58a1799a7 rearranged inductive package for Isar; wenzelm parents: 12133 diff changeset	8	Paulson.
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	9	*)
a5a9c433f639 Initial revision clasohm parents: diff changeset	10
a5a9c433f639 Initial revision clasohm parents: diff changeset	11	val banner = "ZF Set Theory (in FOL)";
a5a9c433f639 Initial revision clasohm parents: diff changeset	12	writeln banner;
a5a9c433f639 Initial revision clasohm parents: diff changeset	13
12175 5cf58a1799a7 rearranged inductive package for Isar; wenzelm parents: 12133 diff changeset	14	reset eta_contract;
2469 b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: 1512 diff changeset	15
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	16	print_depth 1;
a5a9c433f639 Initial revision clasohm parents: diff changeset	17
12175 5cf58a1799a7 rearranged inductive package for Isar; wenzelm parents: 12133 diff changeset	18	(syntax for old-style theory sections)
5cf58a1799a7 rearranged inductive package for Isar; wenzelm parents: 12133 diff changeset	19	use "thy_syntax";
516 1957113f0d7d installation of new inductive/datatype sections lcp parents: 488 diff changeset	20
9548 15bee2731e43 instantiated Cancel_Numerals for "nat" in ZF paulson parents: 9211 diff changeset	21	use "~~/src/Provers/Arith/cancel_numerals.ML";
9570 e16e168984e1 installation of cancellation simprocs for the integers paulson parents: 9548 diff changeset	22	use "~~/src/Provers/Arith/combine_numerals.ML";
9548 15bee2731e43 instantiated Cancel_Numerals for "nat" in ZF paulson parents: 9211 diff changeset	23
12552 d2d2ab3f1f37 separation of the AC part of Main into Main_ZFC, plus a few new lemmas paulson parents: 12183 diff changeset	24	with_path "Integ" use_thy "Main_ZFC";
8127 68c6159440f1 new lemmas for Ntree recursor example; more simprules; more lemmas borrowed paulson parents: 6349 diff changeset	25	simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all);
68c6159440f1 new lemmas for Ntree recursor example; more simprules; more lemmas borrowed paulson parents: 6349 diff changeset	26
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	27	print_depth 8;
a5a9c433f639 Initial revision clasohm parents: diff changeset	28
5511 7f52fb755581 leaves subgoal package empty paulson parents: 4271 diff changeset	29	Goal "True"; (leave subgoal package empty)

author	wenzelm
	Tue, 08 Jan 2002 17:32:40 +0100
changeset 12671	bb6db6c0d4df
parent 12552	d2d2ab3f1f37
child 12715	f7299128cd7d
permissions	-rw-r--r--