2006-09-21 paulson 2006-09-21 Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions unless theorems differ by sorts alone, which should not matter. Also minor fixes to standard hashing.
2006-09-21 paulson 2006-09-21 corrected for the translation from _ to __ in c_COMBx_e
2006-09-21 huffman 2006-09-21 changed constants into abbreviations; shortened proofs
2006-09-21 berghofe 2006-09-21 XML syntax for types, terms, and proofs.
2006-09-21 berghofe 2006-09-21 Added xml_syntax.ML
2006-09-21 berghofe 2006-09-21 Added Tools/xml_syntax.ML
2006-09-21 haftmann 2006-09-21 circumvented defect in SML/NJ type inference
2006-09-21 krauss 2006-09-21 1. Function package accepts a parameter (default "some_term"), which specifies the functions behaviour outside its domain. 2. Bugfix: An exception occured when a function in a mutual definition was declared but no equation was given.
2006-09-21 huffman 2006-09-21 removed division_by_zero class requirements from several lemmas
2006-09-21 huffman 2006-09-21 added approx_hnorm theorem; removed division_by_zero class requirements from several lemmas
2006-09-20 isatest 2006-09-20 choose gnuplot terminal by platform
2006-09-20 wenzelm 2006-09-20 set terminal png color -- works for older versions of gnuplot;
2006-09-20 wenzelm 2006-09-20 added ZF-UNITY;
2006-09-20 paulson 2006-09-20 tidied
2006-09-20 mengj 2006-09-20 Added in combinator reduction axioms for B' C' and S'. Also split the original reduction axioms into separate files: I+K, B+C, S, B'+C', S'.
2006-09-20 isatest 2006-09-20 make it work on sunbroy2
2006-09-20 mengj 2006-09-20 Moved the functional equality axioms to helper1 files.
2006-09-20 mengj 2006-09-20 Introduced combinators B', C' and S'.
2006-09-20 mengj 2006-09-20 Removed include_min_comb and include_combS.
2006-09-20 aspinall 2006-09-20 Add Source.of_instream_slurp to try to ensure that XML parser sees whole documents.
2006-09-20 haftmann 2006-09-20 improvements for codegen 2
2006-09-20 haftmann 2006-09-20 name shifts
2006-09-20 haftmann 2006-09-20 fixed bug
2006-09-20 krauss 2006-09-20 Removed "induct set" attribute from total induction rules
2006-09-20 haftmann 2006-09-20 removed debug
2006-09-20 krauss 2006-09-20 Fixed error in pattern splitting algorithm
2006-09-20 huffman 2006-09-20 change section to subsection
2006-09-20 huffman 2006-09-20 add header
2006-09-20 wenzelm 2006-09-20 renamed axclass_xxxx axclasses;
2006-09-19 wenzelm 2006-09-19 tuned;
2006-09-19 wenzelm 2006-09-19 added standard;
2006-09-19 wenzelm 2006-09-19 added name_classrel/arities/arity;
2006-09-19 wenzelm 2006-09-19 pretty_full_theory: suppress internal entities by default;
2006-09-19 wenzelm 2006-09-19 Logic.name_classrel/arities;
2006-09-19 wenzelm 2006-09-19 revert to previous version;
2006-09-19 wenzelm 2006-09-19 added General/susp.ML;
2006-09-19 wenzelm 2006-09-19 removed duplicate arities;
2006-09-19 wenzelm 2006-09-19 sko/abs: Name.internal prevents choking of print_theory;
2006-09-19 wenzelm 2006-09-19 tuned method setup;
2006-09-19 wenzelm 2006-09-19 tuned proofs;
2006-09-19 wenzelm 2006-09-19 'print_theory': bang option for full verbosity;
2006-09-19 wenzelm 2006-09-19 * Pure: 'print_theory' now suppresses entities with internal name;
2006-09-19 wenzelm 2006-09-19 tuned;
2006-09-19 wenzelm 2006-09-19 simple html output;
2006-09-19 wenzelm 2006-09-19 timespan: 100 days;
2006-09-19 wenzelm 2006-09-19 superceded by isatest-statistics;
2006-09-19 wenzelm 2006-09-19 tuned;
2006-09-19 wenzelm 2006-09-19 target dir; proper time formats;
2006-09-19 wenzelm 2006-09-19 Standard statistics.
2006-09-19 wenzelm 2006-09-19 time: include year;
2006-09-19 wenzelm 2006-09-19 Produce statistics from isatest session logs.
2006-09-19 wenzelm 2006-09-19 moved Import/susp.ML to Pure/General;
2006-09-19 obua 2006-09-19 renamed axclass_xxxx axclasses
2006-09-19 haftmann 2006-09-19 removed diagnostic messages
2006-09-19 haftmann 2006-09-19 Operational Equality
2006-09-19 urbanc 2006-09-19 this file contains a compile-challenge suggested by Adam Chlipala; so far it contains only the definition and no proofs
2006-09-19 urbanc 2006-09-19 tuned
2006-09-19 haftmann 2006-09-19 added auxiliary lemma for code generation 2
2006-09-19 haftmann 2006-09-19 removed
2006-09-19 haftmann 2006-09-19 moved part of normalization oracle here