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
2006-09-19 haftmann 2006-09-19 classical arity syntax
2006-09-19 haftmann 2006-09-19 added codegen_data
2006-09-19 haftmann 2006-09-19 moved base setup for evaluation oracle hier
2006-09-19 haftmann 2006-09-19 added OperationalEquality.thy
2006-09-19 haftmann 2006-09-19 code generation 2 adjustments
2006-09-19 haftmann 2006-09-19 (void)
2006-09-19 haftmann 2006-09-19 improved numeral handling for nbe
2006-09-19 haftmann 2006-09-19 added suspensions in Pure
2006-09-19 haftmann 2006-09-19 added some stuff for code generation 2
2006-09-19 haftmann 2006-09-19 dropped error-prone code generation 2 for wfrec
2006-09-19 haftmann 2006-09-19 text cleanup
2006-09-19 haftmann 2006-09-19 introduced syntactic classes; moved some setup to Pure/codegen, Pure/nbe or OperationalEquality.thy
2006-09-19 haftmann 2006-09-19 explicit divmod algorithm for code generation
2006-09-19 haftmann 2006-09-19 added operational equality
2006-09-19 haftmann 2006-09-19 added section on code generation 2
2006-09-19 haftmann 2006-09-19 code_gen now peek keyword
2006-09-19 haftmann 2006-09-19 cleanupdiff
2006-09-19 huffman 2006-09-19 added classes real_div_algebra and real_field; added lemmas
2006-09-19 huffman 2006-09-19 add Real/RealVector.thy
2006-09-18 wenzelm 2006-09-18 * Pure: 'class_deps' command visualizes the subclass relation;
2006-09-18 wenzelm 2006-09-18 added class_deps;
2006-09-18 wenzelm 2006-09-18 added dest_arg, i.e. a tuned version of #2 o dest_comb;
2006-09-18 wenzelm 2006-09-18 Thm.dest_arg;
2006-09-18 wenzelm 2006-09-18 Present.display_graph;
2006-09-18 wenzelm 2006-09-18 added display_graph (from thm_deps.ML);