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
2008-01-14 huffman 2008-01-14 use new-style class for po
2008-01-14 huffman 2008-01-14 add lemma contI2
2008-01-14 huffman 2008-01-14 converted adm_all and adm_ball to rule_format; cleaned up
2008-01-13 berghofe 2008-01-13 Equations for constants without arguments are now declared using "val" instead of "fun".
2008-01-10 huffman 2008-01-10 new theory defining set as a pcpo
2008-01-10 berghofe 2008-01-10 Test data generation and conversion to terms are now more closely intertwined, to allow displaying of functions in test data.
2008-01-10 berghofe 2008-01-10 New example involving functions.
2008-01-10 berghofe 2008-01-10 Now uses more carefully designed simpsets to prevent proofs from failing for some strange datatypes with nested recursion.
2008-01-10 berghofe 2008-01-10 Test data generation and conversion to terms is now more closely intertwined, to allow displaying of functions in test data.
2008-01-10 berghofe 2008-01-10 Eliminated DatatypeAux.dest_TFree to avoid clashes with Term.dest_TFree.
2008-01-10 berghofe 2008-01-10 Added nil_const and cons_const.
2008-01-10 berghofe 2008-01-10 Added test data generator for function type (from Pure/codegen.ML).
2008-01-10 berghofe 2008-01-10 New interface for test data generators.
2008-01-10 huffman 2008-01-10 declare ch2ch_LAM [simp]
2008-01-10 haftmann 2008-01-10 added overloading target