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.
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
Added swap_prems_rl
19960522, by nipkow
Added additional parent theory equalities because some proofs in
19960521, by berghofe
Replaced fast_tac by Fast_tac (which uses default claset)
19960521, by berghofe
Corrected comment wrt I
19960521, by nipkow
Updated url.
19960521, by nipkow
Added thm I_complete_wrt_W to I.
19960520, by nipkow
replaced result() by qed "sorted_insort" in last proof
19960520, by berghofe
Added missing default clause  top_const _ = None;
19960517, by nipkow
Added if_image_distrib.
19960517, by nipkow
Had to rename params because variable names in an induction rule changed.
19960517, by nipkow
Moved split_rule et al from ind_syntax.ML to Prod.ML.
19960517, by nipkow
less
more

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