isabelle: src/ZF/ROOT.ML@7da872d34ace (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
12552 d2d2ab3f1f37 separation of the AC part of Main into Main_ZFC, plus a few new lemmas paulson parents: 12183 diff changeset	16	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	17
5511 7f52fb755581 leaves subgoal package empty paulson parents: 4271 diff changeset	18	Goal "True"; (leave subgoal package empty)

author	webertj
	Wed, 14 Mar 2007 01:35:02 +0100
changeset 22441	7da872d34ace
parent 17935	c6f1442ce949
child 23146	0bc590051d95
permissions	-rw-r--r--