src/ZF/ROOT.ML

ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
the keyword "inductive" making the theory file fail

ZF/Makefile: now has Inductive.thy,.ML

ZF/Datatype,Finite,Zorn: depend upon Inductive
ZF/intr_elim: now checks that the inductive name does not clash with
existing theory names
ZF/ind_section: deleted things replicated in Pure/section_utils.ML
ZF/ROOT: now loads Pure/section_utils

(*  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     "../Pure/section_utils.ML";
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")]);
init_thy_reader ();

use_thy "InfDatatype";
use_thy "List";
use_thy "EquivClass";

(*printing functions are inherited from FOL*)
print_depth 8;

val ZF_build_completed = ();	(*indicate successful build*)