src/ZF/ROOT.ML
 author lcp Tue, 16 Aug 1994 18:58:42 +0200 changeset 532 851df239ac8b parent 516 1957113f0d7d child 578 efc648d29dd0 permissions -rw-r--r--
ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
```
(*  Title: 	ZF/ROOT
ID:         \$Id\$
Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright   1993  University of Cambridge

Adds Zermelo-Fraenkel Set Theory to a database containing First-Order Logic.

This theory is the work of Martin Coen, Philippe Noel and Lawrence Paulson.
*)

val banner = "ZF Set Theory (in FOL)";
writeln banner;

(*For Pure/tactic??  A crude way of adding structure to rules*)
fun CHECK_SOLVED (Tactic tf) =
Tactic (fn state =>
case Sequence.pull (tf state) of
None => error"DO_GOAL: tactic list failed"
| Some(x,_) =>
if has_fewer_prems 1 x then
Sequence.cons(x, Sequence.null)
else (writeln"DO_GOAL: unsolved goals!!";
writeln"Final proof state was ...";
print_goals (!goals_limit) x;
raise ERROR));

fun DO_GOAL tfs = SELECT_GOAL (CHECK_SOLVED (EVERY1 tfs));

print_depth 1;

(*Add user sections for inductive/datatype definitions*)
use_thy "Datatype";
structure ThySyn = ThySynFun
(val user_keywords = ["inductive", "coinductive", "datatype", "codatatype",
"and", "|", "<=", "domains", "intrs", "monos",
"con_defs", "type_intrs", "type_elims"]
and user_sections = [("inductive",  inductive_decl ""),
("coinductive",  inductive_decl "Co"),
("datatype",  datatype_decl ""),
("codatatype",  datatype_decl "Co")]);