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
 clasohm@0 ` 1` ```(* Title: ZF/ROOT ``` lcp@6 ` 2` ``` ID: \$Id\$ ``` clasohm@0 ` 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 ``` lcp@5 ` 18` ``` None => error"DO_GOAL: tactic list failed" ``` lcp@5 ` 19` ``` | Some(x,_) => ``` lcp@5 ` 20` ``` if has_fewer_prems 1 x then ``` lcp@5 ` 21` ``` Sequence.cons(x, Sequence.null) ``` lcp@5 ` 22` ``` else (writeln"DO_GOAL: unsolved goals!!"; ``` lcp@5 ` 23` ``` writeln"Final proof state was ..."; ``` lcp@5 ` 24` ``` print_goals (!goals_limit) x; ``` lcp@5 ` 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@1296 ` 43` ```make_chart (); (*make HTML chart*) ``` clasohm@1296 ` 44` clasohm@0 ` 45` ```val ZF_build_completed = (); (*indicate successful build*) ```