added bind_thm

added qed and qed_goal[w]

added qed_goal for meta_iffD

replaced "val ... = result()" by "qed ..."

le_UN_Ord_lt_csucc: added comment

replaced "rules" by "defs"

---------------------------------------------------------------------- Committing in HOLCF Use new translation mechanism and keyword syntax, cinfix.ML no longer needed. Optimized proofs in Cont.ML Modified Files: Cfun1.ML Cfun2.thy Cont.ML Cprod3.thy Makefile README Sprod3.thy Tr2.thy ccc1.thy ----------------------------------------------------------------------

ZF/indrule/mutual_ind_tac: ensured that asm_full_simp_tac ignores any equalities, by adding setmksimps K[]. ZF/indrule/mut_ss: removed Collect_cong; it is redundant.

checks that the recursive sets are Consts before taking them apart! Bug was introduced during the translation to theory sections.

equiv_comp_eq: simplified proof

moved Cantors theorem here from ZF/ex/misc

deepen_tac: modified due to outcome of experiments. Its choice of unsafe rule to expand is still non-deterministic.

added qed_goal[w]

added blank line

tidied proofs, using fast_tac etc. as much as possible

prove_fun: new; no longer depends upon the version in simpdata.ML

data_domain,Codata_domain: removed replicate; now return one single domain

tidied proofs, using fast_tac etc. as much as possible

added comments on alternative uses of type_intrs/elims

modified for new treatment of mutual recursion

the_equality: more careful use of addSIs and addIs

cons_fun_eq: modified strange uses of classical reasoner

moved Cantors theorem to ZF/ZF.ML and ZF/Perm.ML hom_tac: removed to simplify the proof of comp_homs

moved version of Cantors theorem to ZF/Perm.ML

ZF INDUCTIVE DEFINITIONS: Simplifying the type checking for mutually recursive datatypes, especially with monotone operators Inductive_Fun,CoInductive_Fun: deleted as obsolete inductive_decl: now reads a SINGLE domain for the mutually recursive construction. This could be a sum, perhaps not! CONCRETE SYNTAX has changed too (but there are no examples of this to change).

ZF/Datatype/datatype_decl: supplies a SINGLE domain for the mutually recursive construction. This is [q]univ(A), which is closed under sum.

updated for new deepen_tac

trivial changes

new reference to HO patterns

Pure/tctical/protect_subgoal: simplified to use Sequence.hd Pure/tctical/DEPTH_FIRST: now suppresses duplicate solutions

Pure/term: commented typ_subst_TVars, subst_TVars, subst_Vars, subst_vars

ZF INDUCTIVE DEFINITIONS: Simplifying the type checking for mutually recursive datatypes, especially with monotone operators ZF/add_ind_def/add_fp_def: deleted as obsolete ZF/add_ind_def/add_fp_def_i: now takes dom_sum instead of domts. We no longer automatically construct a sum of separate domains, but could use a sum-closed set such as univ(A).

ZF/intr_elim/elim: now "folds" definitions of the mutually recursive sets!

replaced 'val ... = result();' by 'qed "...";'

ZF/indrule/mutual_ind_tac: backtracks using DEPTH_SOLVE to be certain of solving the subgoal. Entire tactic is enclosed in DETERM to prevent backtracking between subgoals.

ZF/EquivClass/congruent_commuteI: uncommented and simplified proof

ZF/ZF.ML/UN_iff, INT_iff: added to the signature

Pure/thm/norm_term_skip: new, for skipping normalization of the context Pure/thm/bicompose_aux: now computes nlift (number of lifted assumptions in new subgoals) and avoids normalizing the first nlift assumptions in the case where the proof state is not affected. Pure/thm/norm_term_skip: now normalizes types of parameters Pure/thm/THM: aligned colons

Pure/sequence: added comment explaining that memoing sequences were found to be much slower (due to overheads) than the sequences currently used.

Pure/envir/norm_term: replaced equality test for [] by null

page 157 erratum

now searches all subdirectories of object-logics whether or not they are called "ex"

Chnaged simplifier description (lhss)

added call of store_theory after thy file has been read

Updated description of valid lhss.

In ZF, type i has class term, not (just) logic

added check for newlines not enclosed by '\' inside strings

updated remarks about grammar; added section about ambiguities

exported 'cat';

Pure/tctical/select: now uses cprems_of instead of prems_of and cterm_of: new SELECT_GOAL is MUCH faster

Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations

Added month for Coens thesis

removal of FOL_dup_cs

removal of HOL_dup_cs rotation of arguments in split, nat_case, sum_case, list_case

Provers/hypsubst/REPEATN: deleted; using REPEAT_DETERM_N instead.

Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST, REPEAT_DETERM_SOME: new

FOL/intprover/safe_tac: now uses REPEAT_DETERM_FIRST instead of REPEAT_DETERM

argument swaps in HOL

HOL,ZF/Makefile: enclosed multiple "use" calls in parentheses. This ensures that if one dies, all die. BUT NOT Pure/Makefile, where PolyML.use"POLY" makes the identifier "use" visible.

updated pathnames