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*)