src/ZF/ROOT.ML
 author paulson Tue Sep 22 13:50:57 1998 +0200 (1998-09-22) changeset 5529 4a54acae6a15 parent 5511 7f52fb755581 child 6053 8a1059aa01f0 permissions -rw-r--r--
tidying
```     1 (*  Title:      ZF/ROOT
```
```     2     ID:         \$Id\$
```
```     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
```
```     4     Copyright   1993  University of Cambridge
```
```     5
```
```     6 Adds Zermelo-Fraenkel Set Theory to a database containing First-Order Logic.
```
```     7
```
```     8 This theory is the work of Martin Coen, Philippe Noel and Lawrence Paulson.
```
```     9 *)
```
```    10
```
```    11 val banner = "ZF Set Theory (in FOL)";
```
```    12 writeln banner;
```
```    13
```
```    14 eta_contract:=false;
```
```    15
```
```    16 (*For Pure/tactic??  A crude way of adding structure to rules*)
```
```    17 fun CHECK_SOLVED tac st =
```
```    18     case Seq.pull (tac st) of
```
```    19         None => error"DO_GOAL: tactic list failed"
```
```    20       | Some(x,_) =>
```
```    21                 if has_fewer_prems 1 x then
```
```    22                     Seq.cons(x, Seq.empty)
```
```    23                 else (writeln"DO_GOAL: unsolved goals!!";
```
```    24                       writeln"Final proof state was ...";
```
```    25                       print_goals (!goals_limit) x;
```
```    26                       raise ERROR);
```
```    27
```
```    28 fun DO_GOAL tfs = SELECT_GOAL (CHECK_SOLVED (EVERY1 tfs));
```
```    29
```
```    30 print_depth 1;
```
```    31
```
```    32 (*Add user sections for inductive/datatype definitions*)
```
```    33 use     "\$ISABELLE_HOME/src/Pure/section_utils.ML";
```
```    34 use     "thy_syntax.ML";
```
```    35
```
```    36 use_thy "Let";
```
```    37 use_thy "func";
```
```    38 use     "typechk.ML";
```
```    39 use_thy "InfDatatype";
```
```    40 use_thy "List";
```
```    41
```
```    42 (*Integers & binary integer arithmetic*)
```
```    43 cd "Integ";
```
```    44 use_thy "Bin";
```
```    45 cd "..";
```
```    46
```
```    47 (*the all-in-one theory*)
```
```    48 use_thy "Main";
```
```    49
```
```    50 print_depth 8;
```
```    51
```
```    52 Goal "True";  (*leave subgoal package empty*)
```
```    53
```
```    54 val ZF_build_completed = ();    (*indicate successful build*)
```