src/ZF/ROOT.ML
author paulson
Fri Feb 16 18:00:47 1996 +0100 (1996-02-16)
changeset 1512 ce37c64244c0
parent 1461 6bcb44e4d6e5
child 2469 b50b8c0eec01
permissions -rw-r--r--
Elimination of fully-functorial style.
Type tactic changed to a type abbrevation (from a datatype).
Constructor tactic and function apply deleted.
     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 tac st =
    16     case Sequence.pull (tac st) of
    17         None => error"DO_GOAL: tactic list failed"
    18       | Some(x,_) => 
    19                 if has_fewer_prems 1 x then
    20                     Sequence.cons(x, Sequence.null)
    21                 else (writeln"DO_GOAL: unsolved goals!!";
    22                       writeln"Final proof state was ...";
    23                       print_goals (!goals_limit) x;
    24                       raise ERROR);
    25 
    26 fun DO_GOAL tfs = SELECT_GOAL (CHECK_SOLVED (EVERY1 tfs));
    27 
    28 print_depth 1;
    29 
    30 (*Add user sections for inductive/datatype definitions*)
    31 use     "../Pure/section_utils.ML";
    32 use     "thy_syntax.ML";
    33 
    34 use_thy "Let";
    35 use_thy "InfDatatype";
    36 use_thy "List";
    37 use_thy "EquivClass";
    38 
    39 (*printing functions are inherited from FOL*)
    40 print_depth 8;
    41 
    42 val ZF_build_completed = ();    (*indicate successful build*)