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 Safe_step_tac
1996-06-18, by paulson
Translation infixes <->, etc., no longer available at top-level
1996-06-18, by paulson
Addition of setOfList
1996-06-18, by paulson
Removal of list_all
1996-06-18, by paulson
Translation infixes <->, etc., no longer available at top-level
1996-06-18, by paulson
Inserted comment about problem 43
1996-06-17, by paulson
Removed quantification over lists
1996-06-17, by paulson
Now exports Delrules
1996-06-17, by paulson
Converted to use constdefs instead of defs
1996-06-17, by paulson
Explicitly included add_mult_distrib & add_mult_distrib2
1996-06-14, by paulson
New example of greatest common divisor
1996-06-14, by paulson
Added Primes to list of theories in target ex
1996-06-14, by paulson
Now del_simp catches the right exception!
1996-06-14, by paulson
Added delete function for brls
1996-06-14, by paulson
Now implements delrules
1996-06-14, by paulson
Added new Primes theory
1996-06-14, by paulson
Explicitly included add_mult_distrib & add_mult_distrib2
1996-06-14, by paulson
Updated list of theories for target ex
1996-06-14, by paulson
Tidied spacing
1996-06-14, by paulson
New lemmas for gcd example
1996-06-14, by paulson
Obsolete relics concerned with recursion
1996-06-14, by paulson
New example of GCDs and divides relation
1996-06-13, by paulson
The "divides" relation, the greatest common divisor and Euclid's algorithm
1996-06-13, by paulson
Addition of converse_iff, domain_converse, range_converse as rewrites
1996-06-07, by paulson
Quotes now optional around inductive set
1996-06-06, by paulson
Quotes now optional around inductive set
1996-06-06, by paulson
Quotes now optional around inductive set
1996-06-06, by paulson
Tidied some proofs
1996-06-04, by paulson
best_tac, deepen_tac and safe_tac now also use default claset.
1996-06-03, by berghofe
Shortened some proofs
1996-06-03, by paulson
Added a new theorem, UN_Int_subset
1996-06-03, by paulson
Used 2 instead of Suc(Suc 0)
1996-06-03, by paulson
Shortened a proof
1996-06-03, by paulson
adapted use of monofun_cfun_arg
1996-05-31, by oheimb
adapted proof of flat_codom
1996-05-31, by oheimb
introduced forgotten bind_thm calls
1996-05-31, by oheimb
adapted some proofs for new simplifier
1996-05-31, by oheimb
renamed le_0 to le_0_eq, to avoid confusion with le0,
1996-05-31, by oheimb
moved mem_simps and the corresponding update of !simpset from Fun.ML to Set.ML,
1996-05-31, by oheimb
Smaller logo
1996-05-30, by nipkow
Regrouped logo
1996-05-30, by nipkow
Added logo
1996-05-29, by nipkow
An Isabelle logo
1996-05-29, by nipkow
Replaced setsolver by addsolver
1996-05-29, by nipkow
Added addsolver
1996-05-29, by nipkow
Simplified proof of deduction theorem
1996-05-28, by paulson
Corrected a comment in #34
1996-05-28, by paulson
Rules pred_0, pred_Suc etc. are now stored in theorem database.
1996-05-24, by berghofe
Modified proof of "(R^=)^* = R^*" to accommodate equalityI.
1996-05-24, by nipkow
Removed junk introduced by a cvs merge.
1996-05-24, by nipkow
Augmented comment about conversion to clauses
1996-05-24, by paulson
expanded TABs
1996-05-23, by berghofe
equalityI is now added to default claset
1996-05-23, by berghofe
Removed equalityI from some proofs (because it is now included
1996-05-23, by berghofe
Replaced fast_tac by Fast_tac (which uses default claset)
1996-05-23, by berghofe
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
1996-05-22, by nipkow
Added ex_imp
1996-05-22, by nipkow
Added the second half of the W/I correspondence.
1996-05-22, by nipkow
Added swap_prems_rl
1996-05-22, by nipkow
Added additional parent theory equalities because some proofs in
1996-05-21, by berghofe

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

isabelle