2004-04-02 ballarin 2004-04-02 Experimental command for instantiation of locales in proof contexts: instantiate <label>: <loc>
2004-04-02 nipkow 2004-04-02 ignore_neq also influences arith_tac now, not just fast_arith_tac
2004-04-02 nipkow 2004-04-02 Added ignore_neq flag.
2004-04-01 paulson 2004-04-01 removal of Binary Trees examples prepratory to its going into AFP
2004-04-01 paulson 2004-04-01 new type class abelian_group
2004-03-31 skalberg 2004-03-31 Added check that Theory.ML does not occur in the files section of the theory Theory.
2004-03-31 nipkow 2004-03-31 Lex now in AFP
2004-03-31 nipkow 2004-03-31 HOL/Lex is now in AFP/Functional-Automata
2004-03-31 streckem 2004-03-31 new
2004-03-30 streckem 2004-03-30 new
2004-03-30 streckem 2004-03-30 Added PSV 2003/2004
2004-03-30 paulson 2004-03-30 tidied
2004-03-30 paulson 2004-03-30 tidied
2004-03-30 nipkow 2004-03-30 Added append_eq_append_conv2
2004-03-29 skalberg 2004-03-29 Added bitvector library (Word) to HOL/Library and a theory using it (Adder) to HOL/ex.
2004-03-29 kleing 2004-03-29 include exercises again
2004-03-29 kleing 2004-03-29 removed intro to isabelle
2004-03-29 kleing 2004-03-29 put in sections, reorganized, removed intro to isabelle
2004-03-29 kleing 2004-03-29 allow sections in contents file
2004-03-26 webertj 2004-03-26 satsolver=dpll
2004-03-26 webertj 2004-03-26 slightly different SAT solver interface
2004-03-26 webertj 2004-03-26 Installed solvers now determined at call time (as opposed to compile time)
2004-03-26 kleing 2004-03-26 symbols in idents
2004-03-25 paulson 2004-03-25 new material from Avigad
2004-03-25 paulson 2004-03-25 new treatment of equivalence classes
2004-03-25 kleing 2004-03-25 documented new identifier syntax
2004-03-25 kleing 2004-03-25 moved MiniML and AVL to archive of formal proofs
2004-03-24 paulson 2004-03-24 auto update
2004-03-24 paulson 2004-03-24 clarified
2004-03-24 paulson 2004-03-24 streamlined treatment of quotients for the integers
2004-03-19 nipkow 2004-03-19 added a few 0 and Suc lemmas
2004-03-19 paulson 2004-03-19 conversion of Hyperreal/Lim to new-style
2004-03-19 paulson 2004-03-19 removed redundant thms
2004-03-19 paulson 2004-03-19 new thms
2004-03-19 paulson 2004-03-19 New simplification ordering to move numerals together. Fixes a bug in the nat cancellation simprocs
2004-03-19 paulson 2004-03-19 stylistic tweaks
2004-03-19 paulson 2004-03-19 Removing the datatype declaration of "order" allows the standard General.order to be used. Thus we can use Int.compare and String.compare instead of the slower home-grown versions.
2004-03-17 berghofe 2004-03-17 case_tac no longer raises THM exception if goal number is out of range.
2004-03-15 paulson 2004-03-15 auto update
2004-03-15 paulson 2004-03-15 heavy tidying
2004-03-15 paulson 2004-03-15 heavy tidying
2004-03-15 paulson 2004-03-15 new lemma
2004-03-15 paulson 2004-03-15 more up-to-date error msg
2004-03-12 webertj 2004-03-12 \<dots> replaced by ...
2004-03-11 webertj 2004-03-11 refute
2004-03-11 webertj 2004-03-11 Documentation updated
2004-03-11 webertj 2004-03-11 Refute_Examples added/fixed
2004-03-11 kleing 2004-03-11 look for multi platform poly first, choose shrink wrapped poly-4.1.3 (guess) only if no multi platform installation found.
2004-03-11 webertj 2004-03-11 SML/NJ compatibility fixes
2004-03-10 webertj 2004-03-10 added Refute_Examples.thy
2004-03-10 webertj 2004-03-10 changed default values for refute
2004-03-10 webertj 2004-03-10 *** empty log message ***
2004-03-10 webertj 2004-03-10 support for non-recursive IDTs, The, arbitrary, Hilbert_Choice.Eps
2004-03-10 webertj 2004-03-10 Updated examples
2004-03-10 webertj 2004-03-10 *** empty log message ***
2004-03-10 webertj 2004-03-10 Internal and external SAT solvers
2004-03-10 webertj 2004-03-10 Formulas of propositional logic
2004-03-10 webertj 2004-03-10 ZCHAFF_HOME variable added
2004-03-10 paulson 2004-03-10 new thm
2004-03-10 paulson 2004-03-10 strengthened the axclass claims