function names in when_rews now meta-quantified

when_funs removed

*** empty log message ***

Initial revision

Changed argument order of nat_rec.

Changed argument order of nat_rec.

Replaced occurrence of fast_tac by Fast_tac .

Replaced occurrence of set_cs by claset_of "Fun" .

Added function Addss.

Classical tactics now use default claset.

minor fix of index_vnames: name "O" is occupied (used in HOL/Relation.thy)

Restored Addsimps [Suc_le_lessD], as it cannot be added to base HOL

Corrected comment

New rewrites for vacuous quantification

Addition of setOfList

Addition of Safe_step_tac

Translation infixes <->, etc., no longer available at top-level

Addition of setOfList

Removal of list_all

Translation infixes <->, etc., no longer available at top-level

Inserted comment about problem 43

Removed quantification over lists

Now exports Delrules

Converted to use constdefs instead of defs

Explicitly included add_mult_distrib & add_mult_distrib2

New example of greatest common divisor

Added Primes to list of theories in target ex

Now del_simp catches the right exception!

Added delete function for brls

Now implements delrules

Added new Primes theory

Explicitly included add_mult_distrib & add_mult_distrib2

Updated list of theories for target ex

Tidied spacing

New lemmas for gcd example

Obsolete relics concerned with recursion

New example of GCDs and divides relation

The "divides" relation, the greatest common divisor and Euclid's algorithm

Addition of converse_iff, domain_converse, range_converse as rewrites

Quotes now optional around inductive set

Quotes now optional around inductive set

Quotes now optional around inductive set

Tidied some proofs

best_tac, deepen_tac and safe_tac now also use default claset.

Shortened some proofs

Added a new theorem, UN_Int_subset

Used 2 instead of Suc(Suc 0)

Shortened a proof

adapted use of monofun_cfun_arg

adapted proof of flat_codom

introduced forgotten bind_thm calls

adapted some proofs for new simplifier

renamed le_0 to le_0_eq, to avoid confusion with le0, supplied an experimental thm Suc_le_eq, but commented it out

moved mem_simps and the corresponding update of !simpset from Fun.ML to Set.ML, as there have been unnecessary proofs of anonymous thms, which could not be removed (by name) from the !simpset where necessary. All these thms except singleton_iff were already proved in Set.ML. therefore in Set.ML: New version of singletonE, proof of new thm singleton_iff

Smaller logo

Regrouped logo

Added logo

An Isabelle logo

Replaced setsolver by addsolver

Added addsolver

Simplified proof of deduction theorem

Corrected a comment in #34

Rules pred_0, pred_Suc etc. are now stored in theorem database.

Modified proof of "(R^=)^* = R^*" to accommodate equalityI.

Removed junk introduced by a cvs merge.

Augmented comment about conversion to clauses

expanded TABs

equalityI is now added to default claset

Removed equalityI from some proofs (because it is now included in the default claset)

Replaced fast_tac by Fast_tac (which uses default claset) New rules are now also added to default claset.

Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s

Added ex_imp

Added the second half of the W/I correspondence.

Added swap_prems_rl

Added additional parent theory equalities because some proofs in Prod.ML depend on rules proved in equalities.ML

Replaced fast_tac by Fast_tac (which uses default claset) New rules are now also added to default claset.

Corrected comment wrt I

Updated url.

Added thm I_complete_wrt_W to I. Added a few lemmas to Maybe and Type.

replaced result() by qed "sorted_insort" in last proof

Added missing default clause | top_const _ = None;

Added if_image_distrib.

Had to rename params because variable names in an induction rule changed.

Moved split_rule et al from ind_syntax.ML to Prod.ML. Used split_rule in Lfp.ML and Trancl.ML.

Deleted spurious line break

Corrected and augmented timings

Updated for new form of induction rules

Updated for new form of induction rules

Removed special syntax for -a-> and nested tuples to left

Updated for new form of induction rules

Added prune_params_tac to improve readability of subgoals

moved ap_split to cartprod.ML

Modified to use new functor signatures

Predicates are now uncurried in both induction rules, regardless of how tuples are nested. Only returns mutual_induct if there is true mutual recursion.

Uses new ap_split from cartprod module

New functor for operating on the two forms of Cartesian product

Added new name cartprod

Updated for new form of induction rules

Updated for new form of induction rules

Updated for new form of induction rules

Removal of special syntax for -a-> and -b->

Unfolding of arbitrarily nested tuples in induction rules

Now split_all_tac works for i>1 !

Added function claset_of.

Added function for storing default claset in theory.

Added functions for default claset.

Replaced split_tac by split_inside_tac.

Added split_inside_tac.

Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.

Updated timings; more theorems can be proved

Now mentions but does not load mesontest2.ML

updated comments for handling derivations

Extra examples for safe_meson_tac

Restored a proof of Pelletier #38 -- mysteriously deleted

Added note on types.

Deleted diff_mult_distrib_r as diff_mult_distrib is not proved in Arith.

New cancellation and monotonicity laws, about multiplication and division, from ZF/Arith.

Two new "obvious" examples

Provides merge_cs to support default clasets

Simplified KG's proofs