src/ZF/ROOT.ML
 author wenzelm Tue Nov 13 22:20:51 2001 +0100 (2001-11-13) changeset 12175 5cf58a1799a7 parent 12133 f314630235a4 child 12183 c10cea75dd56 permissions -rw-r--r--
rearranged inductive package for Isar;
```     1 (*  Title:      ZF/ROOT.ML
```
```     2     ID:         \$Id\$
```
```     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
```
```     4     Copyright   1993  University of Cambridge
```
```     5
```
```     6 Zermelo-Fraenkel Set Theory on top of classical First-Order Logic.
```
```     7 This theory is the work of Martin Coen, Philippe Noel and Lawrence
```
```     8 Paulson.
```
```     9 *)
```
```    10
```
```    11 val banner = "ZF Set Theory (in FOL)";
```
```    12 writeln banner;
```
```    13
```
```    14 reset eta_contract;
```
```    15
```
```    16 print_depth 1;
```
```    17
```
```    18 (*syntax for old-style theory sections*)
```
```    19 use "thy_syntax";
```
```    20
```
```    21 use "~~/src/Provers/Arith/cancel_numerals.ML";
```
```    22 use "~~/src/Provers/Arith/combine_numerals.ML";
```
```    23
```
```    24 use_thy "mono";
```
```    25 use "ind_syntax.ML";
```
```    26 use_thy "Datatype";
```
```    27
```
```    28 use     "Tools/numeral_syntax.ML";
```
```    29 (*the all-in-one theory*)
```
```    30 with_path "Integ" use_thy "Main";
```
```    31
```
```    32 simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all);
```
```    33
```
```    34 print_depth 8;
```
```    35
```
```    36 Goal "True";  (*leave subgoal package empty*)
```