2008-01-25 wenzelm 2008-01-25 tuned document;
2008-01-25 wenzelm 2008-01-25 tuned;
2008-01-25 wenzelm 2008-01-25 * Default settings: PROOFGENERAL_OPTIONS no longer impose xemacs here;
2008-01-25 haftmann 2008-01-25 tuned
2008-01-25 haftmann 2008-01-25 print postprocessor equations
2008-01-25 haftmann 2008-01-25 fixed and tuned
2008-01-25 haftmann 2008-01-25 dropped superfluous code theorems
2008-01-25 haftmann 2008-01-25 improved code theorem setup
2008-01-25 haftmann 2008-01-25 consistent interacitve bootstrap of HOL-Main
2008-01-25 haftmann 2008-01-25 distinguished examples for Efficient_Nat.thy
2008-01-25 haftmann 2008-01-25 clarified setup of method "normalization"
2008-01-25 haftmann 2008-01-25 moved definition of power on ints to theory Int
2008-01-24 wenzelm 2008-01-24 removed unused properties; replaced ContextPosition by Position.thread_data;
2008-01-24 wenzelm 2008-01-24 replaced ContextPosition by Position.thread_data;
2008-01-24 wenzelm 2008-01-24 statement: keep explicit position; replaced ContextPosition by Position.thread_data;
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]