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
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScriptenabled browsers.
New rewrites for vacuous quantification
19960618, by paulson
Addition of setOfList
19960618, by paulson
Addition of Safe_step_tac
19960618, by paulson
Translation infixes <>, etc., no longer available at toplevel
19960618, by paulson
Addition of setOfList
19960618, by paulson
Removal of list_all
19960618, by paulson
Translation infixes <>, etc., no longer available at toplevel
19960618, by paulson
Inserted comment about problem 43
19960617, by paulson
Removed quantification over lists
19960617, by paulson
Now exports Delrules
19960617, by paulson
Converted to use constdefs instead of defs
19960617, by paulson
Explicitly included add_mult_distrib & add_mult_distrib2
19960614, by paulson
New example of greatest common divisor
19960614, by paulson
Added Primes to list of theories in target ex
19960614, by paulson
Now del_simp catches the right exception!
19960614, by paulson
Added delete function for brls
19960614, by paulson
Now implements delrules
19960614, by paulson
Added new Primes theory
19960614, by paulson
Explicitly included add_mult_distrib & add_mult_distrib2
19960614, by paulson
Updated list of theories for target ex
19960614, by paulson
Tidied spacing
19960614, by paulson
New lemmas for gcd example
19960614, by paulson
Obsolete relics concerned with recursion
19960614, by paulson
New example of GCDs and divides relation
19960613, by paulson
The "divides" relation, the greatest common divisor and Euclid's algorithm
19960613, by paulson
Addition of converse_iff, domain_converse, range_converse as rewrites
19960607, by paulson
Quotes now optional around inductive set
19960606, by paulson
Quotes now optional around inductive set
19960606, by paulson
Quotes now optional around inductive set
19960606, by paulson
Tidied some proofs
19960604, by paulson
best_tac, deepen_tac and safe_tac now also use default claset.
19960603, by berghofe
Shortened some proofs
19960603, by paulson
Added a new theorem, UN_Int_subset
19960603, by paulson
Used 2 instead of Suc(Suc 0)
19960603, by paulson
Shortened a proof
19960603, by paulson
adapted use of monofun_cfun_arg
19960531, by oheimb
adapted proof of flat_codom
19960531, by oheimb
introduced forgotten bind_thm calls
19960531, by oheimb
adapted some proofs for new simplifier
19960531, by oheimb
renamed le_0 to le_0_eq, to avoid confusion with le0,
19960531, by oheimb
moved mem_simps and the corresponding update of !simpset from Fun.ML to Set.ML,
19960531, by oheimb
Smaller logo
19960530, by nipkow
Regrouped logo
19960530, by nipkow
Added logo
19960529, by nipkow
An Isabelle logo
19960529, by nipkow
Replaced setsolver by addsolver
19960529, by nipkow
Added addsolver
19960529, by nipkow
Simplified proof of deduction theorem
19960528, by paulson
Corrected a comment in #34
19960528, by paulson
Rules pred_0, pred_Suc etc. are now stored in theorem database.
19960524, by berghofe
Modified proof of "(R^=)^* = R^*" to accommodate equalityI.
19960524, by nipkow
Removed junk introduced by a cvs merge.
19960524, by nipkow
Augmented comment about conversion to clauses
19960524, by paulson
expanded TABs
19960523, by berghofe
equalityI is now added to default claset
19960523, by berghofe
Removed equalityI from some proofs (because it is now included
19960523, by berghofe
Replaced fast_tac by Fast_tac (which uses default claset)
19960523, by berghofe
Added comparison with implicit rule Fun(lift s 0 @ Var 0) e> s
19960522, by nipkow
Added ex_imp
19960522, by nipkow
Added the second half of the W/I correspondence.
19960522, by nipkow
less
more

(0)
1000
300
100
60
+60
+100
+300
+1000
+3000
+10000
+30000
tip