2008-02-25 chaieb 2008-02-25 Uses Univ_Poly.thy
2008-02-25 chaieb 2008-02-25 Does not import Poly anymore
2008-02-25 chaieb 2008-02-25 Includes the derivates of polynomials -- reals specific content of Poly
2008-02-25 chaieb 2008-02-25 Two simple theorems about cmod moved to Complex.thy
2008-02-25 chaieb 2008-02-25 Now imports Funamental_Theorem_Algebra
2008-02-25 chaieb 2008-02-25 Added trivial theorems aboud cmod
2008-02-25 chaieb 2008-02-25 Included theories Library/Univ_Poly.thy and Complex/Fundamental_Theorem_Algebra.thy ; Theory Hyperreal/Poly.thy Removed
2008-02-22 krauss 2008-02-22 removed dead code; some cleanup
2008-02-22 haftmann 2008-02-22 non-operative code antiquotation
2008-02-22 haftmann 2008-02-22 non-operative code antiquotation
2008-02-22 haftmann 2008-02-22 added further interface for reading constants
2008-02-22 haftmann 2008-02-22 added first version of datatype antiquotation
2008-02-22 haftmann 2008-02-22 moved refute_tac to linarith.ML
2008-02-21 wenzelm 2008-02-21 more elaborate structure Distribution (filled-in by makedist);
2008-02-21 wenzelm 2008-02-21 keep ChangeLog.gz within distribution; more elaborate structure Distribution (filled-in by makedist);
2008-02-21 wenzelm 2008-02-21 removed junk;
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