Old version of mutual induction never worked. Now ensures that all predicates get the SAME type. Updated mutual_ind_tac from ZF version

Changed comments

Added Part_Int and Part_Collect for inductive definitions

Includes Sum.thy as a parent for mutual recursion

now uses proof209.sty

trivial update

trivial update

finally deleted

Updated nipkow-prehofer

moved mixfix syntax from sign.ML

moved mixfix syntax to Syntax/mixfix.ML

Added insert_not_empty, UN_empty and UN_insert (to set_ss).

added cargs for curried function application

removed debugging output

remove Old_HOL

added comments; fixed a bug; reduced memory usage slightly

added mention of new theories BT and Perm

new inductive definition: permutations

Renamed some vars.

fixed comment

Proof of n_leaves_reflect uses permutative rewriting.

Added function rev and its properties length_rev, etc.

The curried version of HOLCF is now just called HOLCF. The old uncurried version is no longer supported

New theory and proofs including preorder, inorder, ..., initially from ZF/ex/BT. Demonstrates datatypes and primrec.

renamed CHOL to HOL

renamed CHOL to HOL

renamed CHOL to HOL

changed 'chol' labels to 'hol'; added a few parentheses

changes made by Lawrence Paulson

Minimal proof tuning.

added add_trrules_i; cleaned up signature THM; improved some comments;

added add_trrules_i;

added extend_trrules_i;

added a few comments on ThyInfo

Put in direct proof of C-R w/o detour via cd.

removed \...\ inside strings

changed call of store_thm_db so that it's result is not displayed by PolyML or SML

Simplified the confluence proofs. Added optimized substitution.

Added add_lessD1

removed \...\ inside strings

removed \...\ inside strings

removed \...\ inside strings

Added remark that \...\ in strings is unnecessary.

removed 'raw' productions from gram datatype; replaced mk_gram by add_prods; completely changed the generation of internal grammars to reuse existing ones in extend_gram

added CHOL

fixed bug in mfix_to_xprod: lambda productions' lhs shouldn't be modified

converted to LaTeX-2e

Now string_of_vname checks for the empty variable name, catching the exception LIST.

Corrected comments in headers

commented thms_unifying_with out; placed thm_db into signature again; placed structures ThmDB and Readthy into Pure again; changed init_thy_reader so that thm_db and loaded_thys are preserved (necessary e.g. for ZF)

Added dependence on Thy/thm_database.ML

*** empty log message ***

polish

removed thm_num and thm_db from signature

fixed bug in thms_containing; changed error/warning messages; added thms_resolving_with

fixed bug: ThySynFun really shouldn't be deleted

changed error message in thms_containing

replaced "All" by "all" in ThmdbFUN's ignore parameter

added theorem database which contains axioms and theorems indexed by the constants they contain

Added Church-Rosser

Added trancl_cs

Moved Relation from Integ to main HOL.

Trancl is now based on Relation which used to be in Integ.

changed macro expander such that patterns also match prefixes of appls;

Moved comment from ParRed.thy to ROOT.ML

Added Park induction to Lfp. Added Lambda to Makefile.

Polished the presentation making it completely definitional.

Krzysztof Grabczewski's (nearly) complete AC proofs

renamed trans_rtrancl to rtrancl_trans and modified it by expanding trans.

Added some lemmas about r^*.

Lambda calculus in de Bruijn notation. Proof of confluence.

Indexing of COMP

Indexing of FILTER and COND

show_sorts

Modified translation for pattern abstraction.

Moved induct2 from Hoare to Lfp.

Prod is now a parent of Lfp. Added thm induct2 to Lfp. Changed the way patterns in abstractions are pretty printed. It has become simpler now but fails if split has more than one argument because then the ast-translation does not match.

converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex

added \CHOL

Calls 'rail' program for syntax diagrams

Changed some definitions and proofs to use pattern-matching.

Changed to use split instead of fsplit. The weakening of fsplitE appears not to affect existing proofs.

case is defined using pattern-matching

Modified proofs for new form of 'split'.

Added pattern-matching code from CHOL/Prod.thy. Changed definitions so that split is now defined in terms of fst, snd. Now split is polymorphic. Deleted fsplit, as split(...)::o gives a similar effect -- NOT identical though, as fsplit(P,z) implied that z was a pair, while split(P,z) means only P(fst(z),snd(z)).

Modified proofs for (q)split, fst, snd for new definitions. The rule f(q)splitE is now called (q)splitE and is weaker than before. The rule '(q)split' is now a meta-equality; this required modifying all proofs involving e.g. split RS trans.

Changed to use split instead of fsplit. The weakening of fsplitE appears not to affect existing proofs.

prove_case_equation now calls uses meta_eq_to_obj_eq to cope with new form of 'split'. Tried calling simp_tac instead of using resolution with trans, but it was significantly slower: 98.3 secs instead of 91.2 secs for ex/Enum.

show_sorts:=true forces display of types

trivial rewording

trivial change

Covers wrapper tacticals: setwrapper, ..., addss

fixed bug in thy_unchanged that occurred when the .thy file was changed but the .ML file hadn't been read before; tmpfile is now deleted immediatly after reading the .thy file in use_thy

Changed definitions so that qsplit is now defined in terms of qfst, qsnd. AT PRESENT THERE IS NO PATTERN-MATCHING FOR QSPLIT.

Modified proofs for (q)split, fst, snd for new definitions. The rule f(q)splitE is now called (q)splitE and is weaker than before. The rule '(q)split' is now a meta-equality; this required modifying all proofs involving e.g. split RS trans.

Changed some definitions and proofs to use pattern-matching.

Patterns can now be let-bound

Changed to use split instead of fsplit. The weakening of fsplitE appears not to affect existing proofs.

Changed some definitions and proofs to use pattern-matching.

Changed some definitions and proofs to use pattern-matching.

Changed some definitions and proofs to use pattern-matching.

Now show_sorts:=true causes printing of types

Imported meta_eq_to_obj_eq from HOL for use with 'split'.

replaced store_thm by bind_thm

trivial change

new version

Covers defs and re-ordering of theory sections

Updates involving defs, addss, etc.

Simplified layout a little.

Corrected display of split f t: no more let. Also replaced "_abs" by "_lambda" --- the former was a mistake which happended to work.

Sections can now be given in any order.

Simplified proof of Hausdorff_next_exists.

Added functor f() = struct end to hide functors to save space.

Renamed insert_kbrl to insert_tagged_brl and exported it. Now subgoals_of_brl calls nprems_of, which is faster than length o prems_of.

Modified proofs for new claset primitives. The problem is that they enforce the "most recent added rule has priority" policy more strictly now.

Modified proofs for new claset primitives. The problem is that they enforce the "most recent added rule has priority" policy more strictly now.

Modified proofs for new claset primitives. The problem is that they enforce the "most recent added rule has priority" policy more strictly now.

Recoded addSIs, etc., so that nets are built incrementally instead of from scratch each time. The old approach used excessive time (>1 sec for adding a rule to ZF_cs) and probably excessive space. Now rep_claset includes all record fields. joinrules no longer sorts the rules on number of subgoals, since it does not see the full set of them; instead the number of subgoals modifies the priority.

updated version

Simple updates for compatibility with KG