isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

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

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

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

isabelle