2008-01-24 wenzelm 2008-01-24 improved apply: handle thread position, apply to context here; replaced ContextPosition by Position.thread_position;
2008-01-24 wenzelm 2008-01-24 removed unused Toplevel.properties;
2008-01-24 wenzelm 2008-01-24 added combinator for wrapped lazy evaluation;
2008-01-24 wenzelm 2008-01-24 added setmp_thread_data_seq;
2008-01-24 wenzelm 2008-01-24 removed obsolete context_position.ML (superseded by Position.thread_data);
2008-01-24 wenzelm 2008-01-24 switched to polyml-cvs;
2008-01-24 berghofe 2008-01-24 Reimplemented proof of strong induction theorem.
2008-01-24 berghofe 2008-01-24 Added lemma at_fin_set_fresh.
2008-01-23 wenzelm 2008-01-23 reactivated mk of java/scala sources, with paranoia PATH setting for sunbroy;
2008-01-23 wenzelm 2008-01-23 exceptions: assign result = null properly;
2008-01-23 wenzelm 2008-01-23 tuned proofs;
2008-01-23 wenzelm 2008-01-23 recovered #der example without using val it;
2008-01-23 haftmann 2008-01-23 yet another OCaml fix
2008-01-22 haftmann 2008-01-22 tuned
2008-01-22 haftmann 2008-01-22 added map_split
2008-01-22 haftmann 2008-01-22 added class semiring_div
2008-01-22 haftmann 2008-01-22 fixed OCaml
2008-01-22 haftmann 2008-01-22 avoid 'it' in ML expressions
2008-01-21 berghofe 2008-01-21 Removed Logic.auto_rename.
2008-01-21 haftmann 2008-01-21 Efficient_Nat streamlined and improved
2008-01-21 haftmann 2008-01-21 tuned proof
2008-01-21 haftmann 2008-01-21 non-negative numerals
2008-01-21 haftmann 2008-01-21 tuned
2008-01-21 haftmann 2008-01-21 more lemmas
2008-01-21 haftmann 2008-01-21 proper meaningful examples
2008-01-21 haftmann 2008-01-21 explicit auxiliary function for code setup
2008-01-21 haftmann 2008-01-21 streamlined and improved
2008-01-21 haftmann 2008-01-21 adjusted to constant and theorem renames
2008-01-21 haftmann 2008-01-21 avoiding direct references to numeral presentation
2008-01-21 haftmann 2008-01-21 tuned code setup
2008-01-18 huffman 2008-01-18 add space to binder syntax
2008-01-18 huffman 2008-01-18 pcpodef generates strict_iff lemmas
2008-01-18 huffman 2008-01-18 change lemma admD to rule_format
2008-01-18 haftmann 2008-01-18 improved implementation
2008-01-17 huffman 2008-01-17 convert lemma lub_mono to rule_format
2008-01-17 huffman 2008-01-17 rename lemma chain_mono3 -> chain_mono, chain_mono -> chain_mono_less
2008-01-17 huffman 2008-01-17 change class axiom chfin to rule_format
2008-01-16 huffman 2008-01-16 change class axiom ax_flat to rule_format
2008-01-15 haftmann 2008-01-15 joined theories IntDef, Numeral, IntArith to theory Int
2008-01-15 haftmann 2008-01-15 tuned
2008-01-15 haftmann 2008-01-15 further localization
2008-01-15 haftmann 2008-01-15 explicit code lemma for implication
2008-01-15 huffman 2008-01-15 add instance for class bifinite
2008-01-15 huffman 2008-01-15 clean up some proofs; add lemmas spair_strict_iff, spair_less_iff, spair_eq_iff; add instance for class bifinite
2008-01-15 huffman 2008-01-15 declare cpair_strict [simp]
2008-01-14 isatest 2008-01-14 make at-sml-dev experimental
2008-01-14 huffman 2008-01-14 added bifinite class instance
2008-01-14 huffman 2008-01-14 add bifinite instances
2008-01-14 huffman 2008-01-14 add class bifinite_cpo for possibly-unpointed bifinite domains
2008-01-14 huffman 2008-01-14 cleaned up instance proofs
2008-01-14 huffman 2008-01-14 new-style instantiation proof for unit :: po
2008-01-14 huffman 2008-01-14 class bifinite supersedes class dcpo; remove unnecessary dcpo stuff
2008-01-14 huffman 2008-01-14 simplified chfin instance proof
2008-01-14 huffman 2008-01-14 new theory of powerdomains
2008-01-14 huffman 2008-01-14 new theory of bifinite domains
2008-01-14 huffman 2008-01-14 new-style class instantiation
2008-01-14 huffman 2008-01-14 added lemmas lub_distribs
2008-01-14 nipkow 2008-01-14 *** empty log message ***
2008-01-14 nipkow 2008-01-14 *** empty log message ***
2008-01-14 huffman 2008-01-14 compact_chfin is now declared simp