2007-05-31 ago wenzelm simplified/unified list fold;
2007-05-31 ago huffman replace (- 1) with -1
2007-05-31 ago huffman simplify some proofs
2007-05-31 ago wenzelm tuned headers -- adapted to usual conventions;
2007-05-31 ago wenzelm moved Compute_Oracle from Pure/Tools to Tools;
2007-05-31 ago wenzelm proper theory setup for compute oracle (based on CPure);
2007-05-31 ago wenzelm moved IsaPlanner from Provers to Tools;
2007-05-31 ago wenzelm moved IsaPlanner from Provers to Tools;
2007-05-31 ago wenzelm made aconvc pervasive;
2007-05-31 ago wenzelm moved aconvc to more_thm.ML;
2007-05-31 ago wenzelm tuned ML setup;
2007-05-31 ago wenzelm decode_term: force qualified name into Const;
2007-05-31 ago wenzelm proper loading of ML files (in HOL.thy);
2007-05-31 ago wenzelm HOL_proofs;
2007-05-31 ago wenzelm moved Integ files to canonical place;
2007-05-31 ago wenzelm proper loading of ML files;
2007-05-31 ago wenzelm removed dead code;
2007-05-31 ago wenzelm tuned header;
2007-05-31 ago wenzelm doc: exclude isabelle_isar.pdf;
2007-05-31 ago urbanc tuned the proof
2007-05-31 ago urbanc introduced symmetric variants of the lemmas for alpha-equivalence
2007-05-31 ago wenzelm proper loading of ML files;
2007-05-31 ago wenzelm removed obsolete IFOL.thy/FOL.thy values;
2007-05-31 ago wenzelm proper loading of ML files;
2007-05-31 ago wenzelm tuned header;
2007-05-31 ago wenzelm tuned oracle setup;
2007-05-31 ago wenzelm moved HOLCF tools to canonical place;
2007-05-31 ago wenzelm moved TFL files to canonical place;
2007-05-31 ago wenzelm moved TFL files to canonical place;
2007-05-31 ago wenzelm added src/Tools;
2007-05-31 ago wenzelm fixed title;
2007-05-31 ago wenzelm Tools: generic tools outside of Pure.
2007-05-31 ago wenzelm moved Integ files to canonical place;
2007-05-31 ago wenzelm fixed use_thy "LocalWeakening";
2007-05-31 ago urbanc included new example in the compiling process
2007-05-31 ago urbanc a theory using locally nameless terms and strong induction principles
2007-05-31 ago urbanc tuned the proof
2007-05-31 ago wenzelm emulate later version of TextIO.inputLine;
2007-05-31 ago wenzelm reversed SML B library patches;
2007-05-31 ago wenzelm TextIO.inputLine: use present SML B library version;
2007-05-30 ago wenzelm tuned USEDIR_OPTIONS;
2007-05-30 ago wenzelm removed HOL4 image, which seldom works;
2007-05-30 ago haftmann simplified data setup
2007-05-30 ago haftmann instance: always print sorts on failure
2007-05-30 ago haftmann more example
2007-05-30 ago haftmann fixed typo
2007-05-30 ago haftmann updated
2007-05-30 ago haftmann generalized lemmas
2007-05-30 ago haftmann eliminated strings
2007-05-30 ago haftmann tuned
2007-05-30 ago krauss clarified error message
2007-05-30 ago huffman simplify names of locale interpretations
2007-05-30 ago huffman renamed some lemmas in Complex.thy
2007-05-30 ago huffman cleaned up proofs; reorganized sections; removed redundant lemmas
2007-05-29 ago huffman use new-style instance declarations
2007-05-29 ago huffman instance complex :: banach
2007-05-29 ago huffman add lemma real_sqrt_sum_squares_less
2007-05-29 ago huffman cleaned up some proofs
2007-05-29 ago huffman interpretation bounded_linear_divide
2007-05-29 ago huffman add bounded_linear lemmas