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.
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
overloading target
20080109, by haftmann
tuned
20080109, by nipkow
added simp attributes/ proofs fixed
20080109, by nipkow
added simp attributes
20080109, by nipkow
Finally: no more unproven.
20080109, by nipkow
tuned
20080109, by haftmann
some more primrec
20080109, by haftmann
tuned
20080109, by haftmann
a note on syntax in class context
20080109, by haftmann
a note on syntax
20080109, by haftmann
tuned proofs
20080108, by urbanc
normalization conversion
20080108, by haftmann
tuned comment
20080108, by haftmann
explicit type variables for instantiation
20080108, by haftmann
better error reporting
20080108, by haftmann
less
more

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