isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

Addition of message NS5
1996-08-21, by paulson
Tidying: removing redundant args in classical reasoner calls
1996-08-21, by paulson
Added le_eq_less_Suc; fixed some comments;
1996-08-21, by paulson
Working version of NS, messages 1-4!
1996-08-20, by paulson
Working version of NS, messages 1-3, WITH INTERLEAVING
1996-08-20, by paulson
Added ref to allow suppression of error msgs
1996-08-20, by paulson
New classical reasoner: warns of, and ignores, redundant rules.
1996-08-20, by paulson
Addition of function set_of_list
1996-08-20, by paulson
Some tidying. This brittle proof depends upon
1996-08-20, by paulson
Corrected for new classical reasoner: redundant rules
1996-08-20, by paulson
updated html-link
1996-08-19, by nipkow
Installation of auto_tac; re-organization
1996-08-19, by paulson
Tidied up the proofs
1996-08-19, by paulson
Added impOfSubs
1996-08-19, by paulson
Now less_zeroE is a Safe Elim rule
1996-08-19, by paulson
Improved comment
1996-08-19, by paulson
Added proof of Un_insert_right
1996-08-19, by paulson
Changed precedences to remove ambiguities in r^+ notation
1996-08-19, by paulson
Improved the proof of Problem 38
1996-08-19, by paulson
Added a lot of basic laws, from HOL/simpdata
1996-08-19, by paulson
Renaming of functions, and tidying
1996-08-19, by paulson
Now starts with set_current_thy
1996-08-19, by paulson
Tidied some proofs
1996-08-19, by paulson
Tidied some proofs, maybe using less_SucE
1996-08-19, by paulson
Removal of less_SucE as default SE rule
1996-08-19, by paulson
Renamed setOfList to set_of_list
1996-08-19, by paulson
Minor improvements of the scripts
1996-08-16, by oheimb
Improved (?) wording of error message
1996-08-12, by paulson
Added a new section on Definitions
1996-08-12, by paulson
Rewording: parameters->arguments!
1996-08-12, by paulson
Initial revision of thy_data.ML
1996-08-08, by berghofe
Added function for storing default claset in theory.
1996-08-08, by berghofe
Removed unnecessary Addsimps.
1996-08-08, by berghofe
Simplified primrec definitions.
1996-08-08, by berghofe
Classical tactics now use default claset.
1996-08-02, by berghofe
Simplified primrec definitions.
1996-08-02, by berghofe
Replaced prove_case_cong by Konrad Slinds optimized version.
1996-08-02, by berghofe
Simplified primrec - definitions.
1996-07-30, by berghofe
Now also Deepen_tac and Best_tac are used.
1996-07-30, by berghofe
Classical tactics now use default claset.
1996-07-30, by berghofe
Works up to main theorem, then XXX...X
1996-07-29, by paulson
Added two new distributive laws
1996-07-29, by paulson
Addition of rev_notE
1996-07-26, by paulson
Inserted spaces in error messages to improve readability
1996-07-26, by paulson
Addition of contra_subsetD and rev_contra_subsetD
1996-07-26, by paulson
Removal of cfast_tac
1996-07-26, by paulson
Removed clash with "range" constant
1996-07-26, by paulson
Redefining "range" as a macro -- new proof needed
1996-07-26, by paulson
Auth proofs work up to the XXX...
1996-07-26, by paulson
Proved insert_image
1996-07-26, by paulson
Redefining "range" as a macro
1996-07-26, by paulson
Proved bex_False
1996-07-26, by paulson
unnecessary files removed
1996-07-23, by oheimb
Corrected typo regarding the type of set_oracle
1996-07-23, by paulson
Added insert_commute
1996-07-22, by paulson
Updated BibTeX identifiers
1996-07-22, by paulson
Acknowledged Martin Simons
1996-07-22, by paulson
Corrected typo involving derivations
1996-07-22, by paulson
Classical tactics now use default claset.
1996-07-19, by berghofe
Corrected o_assoc lemma
1996-07-17, by pusch

less more | (0) -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle