isabelle: src/ZF/ROOT.ML@ac7ea72c463b (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
12552 d2d2ab3f1f37 separation of the AC part of Main into Main_ZFC, plus a few new lemmas paulson parents: 12183 diff changeset	21	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	22
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	23	print_depth 8;
a5a9c433f639 Initial revision clasohm parents: diff changeset	24
5511 7f52fb755581 leaves subgoal package empty paulson parents: 4271 diff changeset	25	Goal "True"; (leave subgoal package empty)

author	wenzelm
	Sat, 23 Apr 2005 19:49:08 +0200
changeset 15821	ac7ea72c463b
parent 15481	fc075ae929e4
child 16483	ace3c2b95353
permissions	-rw-r--r--