2008-02-21 nipkow 2008-02-21 moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas
2008-02-21 nipkow 2008-02-21 moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and added some
2008-02-20 wenzelm 2008-02-20 removed NBE;
2008-02-20 wenzelm 2008-02-20 removed ex/NBE.thy;
2008-02-20 huffman 2008-02-20 fix proofs involving ile_def
2008-02-20 haftmann 2008-02-20 tuned structures in arith_data.ML
2008-02-20 haftmann 2008-02-20 using only an relation predicate to construct div and mod
2008-02-20 nipkow 2008-02-20 now in AFP
2008-02-19 wenzelm 2008-02-19 added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
2008-02-19 wenzelm 2008-02-19 removed General/system_process.ML (back to multithreaded version);
2008-02-19 wenzelm 2008-02-19 replaced setpgrp by more elaborate setsid;
2008-02-19 urbanc 2008-02-19 slightly tuned
2008-02-19 berghofe 2008-02-19 Yet another proof of False, this time using the strong case analysis rule.
2008-02-18 haftmann 2008-02-18 tuned
2008-02-18 wenzelm 2008-02-18 system.pl - invoke shell command line (with robust signal handling);
2008-02-18 urbanc 2008-02-18 updated
2008-02-18 urbanc 2008-02-18 added eqvt-flag to subseteq-lemma
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.