src/ZF/ROOT.ML
 author clasohm Tue Oct 24 14:50:24 1995 +0100 (1995-10-24) changeset 1296 ae31bb7774a7 parent 1069 66efd8f90fbd child 1361 90d615b599d9 permissions -rw-r--r--
added calls of init_html and make_chart
```     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 (*For Pure/tactic??  A crude way of adding structure to rules*)
```
```    15 fun CHECK_SOLVED (Tactic tf) =
```
```    16   Tactic (fn state =>
```
```    17     case Sequence.pull (tf state) of
```
```    18 	None => error"DO_GOAL: tactic list failed"
```
```    19       | Some(x,_) =>
```
```    20 		if has_fewer_prems 1 x then
```
```    21 		    Sequence.cons(x, Sequence.null)
```
```    22 		else (writeln"DO_GOAL: unsolved goals!!";
```
```    23 		      writeln"Final proof state was ...";
```
```    24 		      print_goals (!goals_limit) x;
```
```    25 		      raise ERROR));
```
```    26
```
```    27 fun DO_GOAL tfs = SELECT_GOAL (CHECK_SOLVED (EVERY1 tfs));
```
```    28
```
```    29 print_depth 1;
```
```    30
```
```    31 (*Add user sections for inductive/datatype definitions*)
```
```    32 use     "../Pure/section_utils.ML";
```
```    33 use     "thy_syntax.ML";
```
```    34
```
```    35 use_thy "Let";
```
```    36 use_thy "InfDatatype";
```
```    37 use_thy "List";
```
```    38 use_thy "EquivClass";
```
```    39
```
```    40 (*printing functions are inherited from FOL*)
```
```    41 print_depth 8;
```
```    42
```
```    43 make_chart ();   (*make HTML chart*)
```
```    44
```
```    45 val ZF_build_completed = ();	(*indicate successful build*)
```