src/ZF/ROOT.ML
author clasohm
Thu Sep 16 12:20:38 1993 +0200 (1993-09-16)
changeset 0 a5a9c433f639
child 5 75e163863e16
permissions -rw-r--r--
Initial revision
     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/drule??  Multiple resolution infixes*)
    15 infix 0 MRS MRL;
    16 
    17 (*Resolve a list of rules against bottom_rl from right to left*)
    18 fun rls MRS bottom_rl = 
    19   let fun rs_aux i [] = bottom_rl
    20 	| rs_aux i (rl::rls) = rl RSN (i, rs_aux (i+1) rls)
    21   in  rs_aux 1 rls  end;
    22 
    23 fun rlss MRL bottom_rls = 
    24   let fun rs_aux i [] = bottom_rls
    25 	| rs_aux i (rls::rlss) = rls RLN (i, rs_aux (i+1) rlss)
    26   in  rs_aux 1 rlss  end;
    27 
    28 print_depth 1;
    29 use_thy "zf";
    30 
    31 use     "upair.ML";
    32 use     "subset.ML";
    33 use     "pair.ML";
    34 use     "domrange.ML";
    35 use     "func.ML";
    36 use     "equalities.ML";
    37 use     "simpdata.ML";  
    38 
    39 (*further development*)
    40 use_thy "bool";
    41 use_thy "sum";
    42 use_thy "qpair";
    43 use     "mono.ML";
    44 use_thy "fixedpt";
    45 
    46 (*Inductive/co-inductive definitions*)
    47 use     "ind-syntax.ML";
    48 use     "intr-elim.ML";
    49 use     "indrule.ML";
    50 use     "inductive.ML";
    51 use     "co-inductive.ML";
    52 
    53 use_thy "perm";
    54 use_thy "trancl";
    55 use_thy "wf";
    56 use_thy "ordinal";
    57 use_thy "nat";
    58 use_thy "epsilon";
    59 use_thy "arith";
    60 
    61 (*Datatype/co-datatype definitions*)
    62 use_thy "univ";
    63 use_thy "quniv";
    64 use     "constructor.ML";
    65 use     "datatype.ML";
    66 
    67 use     "fin.ML";
    68 use     "list.ML";
    69 use_thy "list-fn";
    70 
    71 (*printing functions are inherited from FOL*)
    72 print_depth 8;
    73 
    74 val ZF_build_completed = ();	(*indicate successful build*)