Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary

shortlog

changelog
 graph 
tags

bookmarks

branches

files

gz

help
less
more

(0)
10000
3000
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.
tuned proof
20080121, by haftmann
nonnegative numerals
20080121, by haftmann
tuned
20080121, by haftmann
more lemmas
20080121, by haftmann
proper meaningful examples
20080121, by haftmann
explicit auxiliary function for code setup
20080121, by haftmann
streamlined and improved
20080121, by haftmann
adjusted to constant and theorem renames
20080121, by haftmann
avoiding direct references to numeral presentation
20080121, by haftmann
tuned code setup
20080121, by haftmann
add space to binder syntax
20080118, by huffman
pcpodef generates strict_iff lemmas
20080118, by huffman
change lemma admD to rule_format
20080118, by huffman
improved implementation
20080118, by haftmann
convert lemma lub_mono to rule_format
20080117, by huffman
rename lemma chain_mono3 > chain_mono, chain_mono > chain_mono_less
20080117, by huffman
change class axiom chfin to rule_format
20080117, by huffman
change class axiom ax_flat to rule_format
20080116, by huffman
joined theories IntDef, Numeral, IntArith to theory Int
20080115, by haftmann
tuned
20080115, by haftmann
further localization
20080115, by haftmann
explicit code lemma for implication
20080115, by haftmann
add instance for class bifinite
20080115, by huffman
clean up some proofs;
20080115, by huffman
declare cpair_strict [simp]
20080115, by huffman
make atsmldev experimental
20080114, by isatest
added bifinite class instance
20080114, by huffman
add bifinite instances
20080114, by huffman
add class bifinite_cpo for possiblyunpointed bifinite domains
20080114, by huffman
cleaned up instance proofs
20080114, by huffman
newstyle instantiation proof for unit :: po
20080114, by huffman
class bifinite supersedes class dcpo; remove unnecessary dcpo stuff
20080114, by huffman
simplified chfin instance proof
20080114, by huffman
new theory of powerdomains
20080114, by huffman
new theory of bifinite domains
20080114, by huffman
newstyle class instantiation
20080114, by huffman
added lemmas lub_distribs
20080114, by huffman
*** empty log message ***
20080114, by nipkow
*** empty log message ***
20080114, by nipkow
compact_chfin is now declared simp
20080114, by huffman
use newstyle class for po
20080114, by huffman
add lemma contI2
20080114, by huffman
converted adm_all and adm_ball to rule_format; cleaned up
20080114, by huffman
Equations for constants without arguments are now declared using
20080113, by berghofe
new theory defining set as a pcpo
20080110, by huffman
Test data generation and conversion to terms are now more closely
20080110, by berghofe
New example involving functions.
20080110, by berghofe
Now uses more carefully designed simpsets to prevent proofs from
20080110, by berghofe
Test data generation and conversion to terms is now more closely
20080110, by berghofe
Eliminated DatatypeAux.dest_TFree to avoid clashes
20080110, by berghofe
Added nil_const and cons_const.
20080110, by berghofe
Added test data generator for function type (from Pure/codegen.ML).
20080110, by berghofe
New interface for test data generators.
20080110, by berghofe
declare ch2ch_LAM [simp]
20080110, by huffman
added overloading target
20080110, by haftmann
new compactness lemmas; removed duplicated flat_less_iff
20080110, by huffman
Compactness subsection with new lemmas
20080110, by huffman
Compactness subsection with some new lemmas
20080110, by huffman
new compactness lemmas
20080110, by huffman
new lemmas max_in_chainI, max_in_chainD
20080110, by huffman
less
more

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