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.
statement: keep explicit position;
20080124, by wenzelm
improved apply: handle thread position, apply to context here;
20080124, by wenzelm
removed unused Toplevel.properties;
20080124, by wenzelm
added combinator for wrapped lazy evaluation;
20080124, by wenzelm
added setmp_thread_data_seq;
20080124, by wenzelm
removed obsolete context_position.ML (superseded by Position.thread_data);
20080124, by wenzelm
switched to polymlcvs;
20080124, by wenzelm
Reimplemented proof of strong induction theorem.
20080124, by berghofe
Added lemma at_fin_set_fresh.
20080124, by berghofe
reactivated mk of java/scala sources, with paranoia PATH setting for sunbroy;
20080123, by wenzelm
exceptions: assign result = null properly;
20080123, by wenzelm
tuned proofs;
20080123, by wenzelm
recovered #der example without using val it;
20080123, by wenzelm
yet another OCaml fix
20080123, by haftmann
tuned
20080122, by haftmann
added map_split
20080122, by haftmann
added class semiring_div
20080122, by haftmann
fixed OCaml
20080122, by haftmann
avoid 'it' in ML expressions
20080122, by haftmann
Removed Logic.auto_rename.
20080121, by berghofe
Efficient_Nat streamlined and improved
20080121, by haftmann
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
less
more

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