isabelle: src/ZF/ROOT.ML@6eab0f1cb0fe (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
12175 5cf58a1799a7 rearranged inductive package for Isar; wenzelm parents: 12133 diff changeset	16	(syntax for old-style theory sections)
5cf58a1799a7 rearranged inductive package for Isar; wenzelm parents: 12133 diff changeset	17	use "thy_syntax";
516 1957113f0d7d installation of new inductive/datatype sections lcp parents: 488 diff changeset	18
12552 d2d2ab3f1f37 separation of the AC part of Main into Main_ZFC, plus a few new lemmas paulson parents: 12183 diff changeset	19	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	20
5511 7f52fb755581 leaves subgoal package empty paulson parents: 4271 diff changeset	21	Goal "True"; (leave subgoal package empty)

author	huffman
	Thu, 22 Sep 2005 18:59:41 +0200
changeset 17584	6eab0f1cb0fe
parent 16483	ace3c2b95353
child 17935	c6f1442ce949
permissions	-rw-r--r--