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