minor bug fix

updated syntax of primrec definitions

replaced setsolver ... by addsolver

Added Msg 3; works up to Says_Server_imp_Key_newK

Corrected indentation

Oracles can now be strings instead of identifiers

Added insert_mono

Added ML reference

Modified to reject certain inputs -- illustrates error handling

Documentation of oracles and their syntax

Simplified syntax of primrec definitions.

Removed a use of eq_cs

Removed the unused eq_cs, and added some distributive laws

Removed the unused rel_eq_cs

Added contra_subsetD and rev_contra_subsetD

Added rev_notE by analogy with rev_mp

Proving safety properties of authentication protocols

Updated reference to Slinds paper on TFL

Now set_cs is just taken from !claset

Added type-checking to rule "combination". This corrects a fault concerning soundness. See Jeremy Dawsons message of 27 Jun 1996 on isabelle-users

Restored warning comment

re-added when_funs to library.ML

patches for Holcfb.thy removed

removed old version of LEAST operator

repaired 8bit pragma

adapted path to 8bit package

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.