2008-02-18 huffman 2008-02-18 proved linorder and wellorder class instances
2008-02-17 wenzelm 2008-02-17 added get_parent (for AWE); tuned;
2008-02-17 wenzelm 2008-02-17 added perl wrapper for robust signal handling;
2008-02-17 huffman 2008-02-17 New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
2008-02-16 wenzelm 2008-02-16 removed spurious PolyML.makestring;
2008-02-16 wenzelm 2008-02-16 replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
2008-02-16 wenzelm 2008-02-16 removed managed_process (cf. General/shell_process.ML); replaced ignore/raise_interrupt by more flexible (un)interruptible combinators; tuned timeLimit: sleep already interruptible by default; schedule: restore attributes of body, instead of forcing interruptible execution;
2008-02-16 wenzelm 2008-02-16 removed managed_process (cf. General/shell_process.ML);
2008-02-16 wenzelm 2008-02-16 exn_message: added TimeLimit.TimeOut; replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
2008-02-16 wenzelm 2008-02-16 export deny_secure;
2008-02-16 wenzelm 2008-02-16 setmp: uninterruptible;
2008-02-16 wenzelm 2008-02-16 System shell processes, with static input/output and propagation of interrupts.
2008-02-16 wenzelm 2008-02-16 added General/system_process.ML;
2008-02-16 huffman 2008-02-16 added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps
2008-02-16 huffman 2008-02-16 added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps
2008-02-15 wenzelm 2008-02-15 support for managed external processes;
2008-02-15 nipkow 2008-02-15 more lemmas
2008-02-15 haftmann 2008-02-15 <= and < on nat no longer depend on wellfounded relations
2008-02-15 haftmann 2008-02-15 moved *_reorient lemmas here
2008-02-15 wenzelm 2008-02-15 tuned names;
2008-02-14 wenzelm 2008-02-14 syntax error: suppress expected categories altogether;
2008-02-14 wenzelm 2008-02-14 expected syntax categories: reduced duplication, report minimal priorities only;
2008-02-14 berghofe 2008-02-14 Fixed typing problem that caused instantiation of induct_aux_rec to go wrong.
2008-02-13 paulson 2008-02-13 make_meta_clause bugfix: now works for higher-order clauses like LeastI_ex
2008-02-13 kleing 2008-02-13 fixed record pretty printing
2008-02-13 haftmann 2008-02-13 using integers for pattern matching
2008-02-13 haftmann 2008-02-13 tuned whitespace
2008-02-13 haftmann 2008-02-13 more abstract lemmas
2008-02-11 huffman 2008-02-11 fix spelling
2008-02-11 wenzelm 2008-02-11 imports Main;
2008-02-11 wenzelm 2008-02-11 removed unnecessary theory qualifiers;
2008-02-11 wenzelm 2008-02-11 simultaneous use_thys;
2008-02-11 wenzelm 2008-02-11 added Id;
2008-02-11 krauss 2008-02-11 Made theory names in ZF disjoint from HOL theory names to allow loading both developments in a single session (but not merge them).
2008-02-11 urbanc 2008-02-11 tuned proofs and comments
2008-02-10 wenzelm 2008-02-10 tuned spaces;
2008-02-10 wenzelm 2008-02-10 tuned default position;
2008-02-10 wenzelm 2008-02-10 added default_properties;
2008-02-10 wenzelm 2008-02-10 added position_properties;
2008-02-10 wenzelm 2008-02-10 maintain default position;
2008-02-09 wenzelm 2008-02-09 overloading: reduced code redundancy, no xstrings here;
2008-02-09 wenzelm 2008-02-09 overloading: tuned signature;
2008-02-07 berghofe 2008-02-07 Instead of raising an exception, pred_set_conv now ignores conversion rules that would cause a clash. This allows multiple interpretations of locales containing inductive sets.
2008-02-07 huffman 2008-02-07 fix broken syntax translations
2008-02-06 huffman 2008-02-06 use ML antiquotations
2008-02-06 krauss 2008-02-06 lemma wf_union_compatible: "wf R ==> wf S ==> S O R <= R ==> wf (R Un S)"
2008-02-06 chaieb 2008-02-06 between constant removed
2008-02-06 haftmann 2008-02-06 continued
2008-02-06 haftmann 2008-02-06 locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
2008-02-04 chaieb 2008-02-04 replaced class by locale
2008-02-04 wenzelm 2008-02-04 *** MESSAGE REFERS TO 1.29 and 1.44 *** sort_of_term: be permissive about _class *output* markers, to allow print translations invoke this function as well;
2008-02-04 haftmann 2008-02-04 towards quickcheck
2008-02-04 haftmann 2008-02-04 suppport for messages and indices
2008-02-04 haftmann 2008-02-04 added indexT
2008-02-02 huffman 2008-02-02 instance "*" :: (sq_ord, sq_ord) sq_ord
2008-02-02 huffman 2008-02-02 cleaned up
2008-02-01 nipkow 2008-02-01 modified MCollect syntax
2008-02-01 haftmann 2008-02-01 <TERM> syntax
2008-02-01 haftmann 2008-02-01 fixed term_of_sort
2008-02-01 haftmann 2008-02-01 fixed record problem