src/ZF/ROOT.ML
 author clasohm Tue Jan 30 13:42:57 1996 +0100 (1996-01-30) changeset 1461 6bcb44e4d6e5 parent 1361 90d615b599d9 child 1512 ce37c64244c0 permissions -rw-r--r--
expanded tabs
 clasohm@1461 1 (* Title: ZF/ROOT lcp@6 2 ID: \$Id\$ clasohm@1461 3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory clasohm@0 4 Copyright 1993 University of Cambridge clasohm@0 5 clasohm@0 6 Adds Zermelo-Fraenkel Set Theory to a database containing First-Order Logic. clasohm@0 7 clasohm@0 8 This theory is the work of Martin Coen, Philippe Noel and Lawrence Paulson. clasohm@0 9 *) clasohm@0 10 clasohm@0 11 val banner = "ZF Set Theory (in FOL)"; clasohm@0 12 writeln banner; clasohm@0 13 lcp@14 14 (*For Pure/tactic?? A crude way of adding structure to rules*) lcp@5 15 fun CHECK_SOLVED (Tactic tf) = lcp@5 16 Tactic (fn state => lcp@5 17 case Sequence.pull (tf state) of clasohm@1461 18 None => error"DO_GOAL: tactic list failed" lcp@5 19 | Some(x,_) => clasohm@1461 20 if has_fewer_prems 1 x then clasohm@1461 21 Sequence.cons(x, Sequence.null) clasohm@1461 22 else (writeln"DO_GOAL: unsolved goals!!"; clasohm@1461 23 writeln"Final proof state was ..."; clasohm@1461 24 print_goals (!goals_limit) x; clasohm@1461 25 raise ERROR)); lcp@5 26 lcp@5 27 fun DO_GOAL tfs = SELECT_GOAL (CHECK_SOLVED (EVERY1 tfs)); lcp@5 28 clasohm@0 29 print_depth 1; clasohm@0 30 lcp@516 31 (*Add user sections for inductive/datatype definitions*) lcp@578 32 use "../Pure/section_utils.ML"; lcp@803 33 use "thy_syntax.ML"; lcp@516 34 lcp@1069 35 use_thy "Let"; lcp@488 36 use_thy "InfDatatype"; lcp@516 37 use_thy "List"; lcp@532 38 use_thy "EquivClass"; clasohm@0 39 clasohm@0 40 (*printing functions are inherited from FOL*) clasohm@0 41 print_depth 8; clasohm@0 42 clasohm@1461 43 val ZF_build_completed = (); (*indicate successful build*)