2009-02-26 wenzelm 2009-02-26 standard headers; eliminated non-ASCII chars, which are fragile in the age of unicode;
2009-02-26 wenzelm 2009-02-26 updated generated files;
2009-02-26 wenzelm 2009-02-26 uniform treatment of ML indexing, using general \indexdef macro for formal Isabelle/Isar entities; more robust handling of "|" within index;
2009-02-26 wenzelm 2009-02-26 fixed import of ~~/src/HOL/Decision_Procs/Ferrack;
2009-02-26 wenzelm 2009-02-26 more explicit indication of old manuals;
2009-02-26 wenzelm 2009-02-26 merged
2009-02-26 wenzelm 2009-02-26 \bibliographystyle{abbrv} for newer ref manuals;
2009-02-26 wenzelm 2009-02-26 added Haftmann-Wenzel:2009;
2009-02-26 wenzelm 2009-02-26 updated generated files;
2009-02-26 wenzelm 2009-02-26 isabelle document: adapted (postulated) defaults for tags to actual isabelle.sty;
2009-02-26 wenzelm 2009-02-26 merged
2009-02-26 wenzelm 2009-02-26 include HOL-Decision_Procs in stats;
2009-02-26 wenzelm 2009-02-26 back to plain http;
2009-02-26 berghofe 2009-02-26 merged
2009-02-26 berghofe 2009-02-26 Added postprocessing rules for fresh_star.
2009-02-26 berghofe 2009-02-26 Fixed nonexhaustive match problem in decomp, to make it fail more gracefully in case assumptions are not of the form (Trueprop $ ...).
2009-02-26 wenzelm 2009-02-26 tuned NEWS;
2009-02-26 wenzelm 2009-02-26 merged
2009-02-26 huffman 2009-02-26 merged
2009-02-26 huffman 2009-02-26 add type annotation
2009-02-26 huffman 2009-02-26 disable floor_minus and ceiling_minus [simp]
2009-02-26 wenzelm 2009-02-26 merged
2009-02-26 paulson 2009-02-26 merged
2009-02-26 paulson 2009-02-26 Updated the theory syntax. Corrected an error in a command.
2009-02-25 huffman 2009-02-25 merged
2009-02-25 huffman 2009-02-25 generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
2009-02-25 huffman 2009-02-25 new theory of Archimedean fields
2009-02-25 huffman 2009-02-25 add lemmas about comparisons of Fract a b with 0 and 1
2009-02-25 huffman 2009-02-25 merged
2009-02-25 huffman 2009-02-25 add lemma diff_Suc_1
2009-02-25 berghofe 2009-02-25 Added lemmas for normalizing freshness results involving fresh_star.
2009-02-25 berghofe 2009-02-25 Added typing and evaluation relations, together with proofs of preservation and progress (i.e. part 2A of the POPLmark challenge).
2009-02-25 berghofe 2009-02-25 merged
2009-02-25 berghofe 2009-02-25 Use LocalTheory.full_name instead of Sign.full_name, because the latter does not work properly for locales.
2009-02-25 berghofe 2009-02-25 Replaced Logic.unvarify by Variable.import_terms to make declaration of equivariance lemmas work in locales.
2009-02-25 berghofe 2009-02-25 nominal_inductive and equivariance now work on local_theory.
2009-02-25 berghofe 2009-02-25 Added equivariance lemmas for fresh_star.
2009-02-25 nipkow 2009-02-25 NEWS
2009-02-25 haftmann 2009-02-25 merged
2009-02-25 haftmann 2009-02-25 robustified
2009-02-24 huffman 2009-02-24 make more proofs work whether or not One_nat_def is a simp rule
2009-02-24 huffman 2009-02-24 add simp rules for numerals with 1::nat
2009-02-24 huffman 2009-02-24 fix lemma hypreal_hnorm_def
2009-02-23 huffman 2009-02-23 make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
2009-02-23 huffman 2009-02-23 move lemma dvd_mod_imp_dvd into class semiring_div
2009-02-23 haftmann 2009-02-23 merged
2009-02-23 haftmann 2009-02-23 improved treatment of case certificates
2009-02-23 haftmann 2009-02-23 repaired order of variable node allocation
2009-02-23 huffman 2009-02-23 explicitly import Fact
2009-02-23 huffman 2009-02-23 change imports to move Fact.thy outside Plain
2009-02-23 huffman 2009-02-23 add lemmas poly_{div,mod}_minus_{left,right}
2009-02-23 huffman 2009-02-23 merged
2009-02-22 huffman 2009-02-22 declare scaleR distrib rules [algebra_simps]; cleaned up
2009-02-22 huffman 2009-02-22 clean up instantiations
2009-02-22 huffman 2009-02-22 merged
2009-02-22 huffman 2009-02-22 simplify some proofs
2009-02-22 huffman 2009-02-22 remove duplicate instance declaration
2009-02-23 haftmann 2009-02-23 stripped classrels_of, instances_of
2009-02-23 haftmann 2009-02-23 use canonical subalgebra projection
2009-02-22 haftmann 2009-02-22 experimental switch to new well-sorting algorithm