New version of datatype.ML with primrec (Norbert). Updated treatment of bounded quantifiers in the simplifier.

INSTALLATION OF INDUCTIVE DEFINITIONS HOL/Sexp, List, LList: updated for inductive defs; streamlined proofs HOL/List, Subst/UTerm, ex/Simult, ex/Term: updated refs to Sexp intr rules HOL/Univ/diag_eqI: new HOL/intr_elim: now checks that the inductive name does not clash with existing theory names HOL/Sum: now type + is an infixr, to agree with type * HOL/Set: added Pow and the derived rules PowI, PowD, Pow_bottom, Pow_top HOL/Fun/set_cs: now includes Pow rules HOL/mono/Pow_mono: new HOL/Makefile: now has Inductive.thy,.ML and ex/Acc.thy,.ML HOL/Sexp,List,LList,ex/Term: converted as follows node *set -> item Sexp -> sexp LList_corec -> <self> LList_ -> llist_ LList\> -> llist List_case -> <self> List_rec -> <self> List_ -> list_ List\> -> list Term_rec -> <self> Term_ -> term_ Term\> -> term

INSTALLATION OF INDUCTIVE DEFINITIONS HOL/ex/MT.thy: now mentions dependence upon Sum.thy HOL/ex/Acc: new example, borrowed & adapted from ZF HOL/ex/Simult, ex/Term: updated refs to Sexp intr rules HOL/Sexp,List,LList,ex/Term: converted as follows node *set -> item Sexp -> sexp LList_corec -> <self> LList_ -> llist_ LList\> -> llist List_case -> <self> List_rec -> <self> List_ -> list_ List\> -> list Term_rec -> <self> Term_ -> term_ Term\> -> term

Subst/UTerm: updated for inductive defs; streamlined proofs

HOL/ex/MT.thy: now mentions dependence upon Sum.thy

new header & minor changes

changed defn to def

HOL/Sum.thy: generalized the type of Part

replaced add_defns_i by add_defs_i; changed instant_types: now uses Sign.infer_types;

HOL/Trancl.thy: depends upon Prod

HOL/Makefile, ROOT: updated for new .thy files

HOL/Ord.thy,.ML: files now have header comments

HOL/Sum: added disjoint sum of two sets as the plus operator, since + is overloaded with an incompatible type

HOL/subset.thy, equalities.thy, mono.thy: new HOL/Lfp.thy: now depends upon mono HOL/Gfp.thy: depends upon Lfp, not just mono

HOL/fun.ML: renamed Fun.ML to avoid problems with MLs "fun" keyword

HOL/ex/Term, Simult: updated for new Split

HOL/List: rotated arguments of List_case, list_case

HOL/Prod: swapped args of split and simplified HOL/Prod/mem_splitI, mem_splitE, prod_cs: new

HOL/Univ: swapped args of split and simplified HOL/Univ: simplified many proofs involving dprod, dsum. HOL/Univ: updated to new nat_case HOL/Univ/univ_cs: added to it and used it more

HOL/Sexp: rotated arguments of Sexp_case

HOL/Nat: rotated arguments of nat_case; added translation for case macro HOL/Nat/nat_ss0: new, for first definition of nat_ss

HOL/Trancl: comp_cs is based upon prod_cs; tidied proofs

HOL/Sum: rotated arguments of sum_case; added translation for case macro HOL/Sum: now has Part primitives, moved from ex/Simult, with extra laws from ZF/Sum

HOL/Subst/AList: swapped args of split and simplified

HOL/LList: swapped args of split and simplified HOL/List: rotated arguments of List_case, list_case HOL/LList: rotated arguments of llist_case (shares List_case) and tidied many proofs

allow long_id for reference to type in primrec. Doesn't work yet, though, because of problems with the autoloader.

Cleaned up code.

Used the new primitive recursive functions format for thy-files

Added primitive recursive functions (Norbert Voelker's code) to the datatype package.

renamed meta_obj_reflection meta_eq_to_obj_eq.