2006-05-16 wenzelm 2006-05-16 abstract interfaces for type algebra; tuned;
2006-05-16 wenzelm 2006-05-16 added divide_and_conquer combinator (by Amine Chaieb); removed remains of old option type; removed obsolete eq_opt; removed obsolete string_of_bool (use Bool.toString instead); tuned;
2006-05-16 wenzelm 2006-05-16 added low-level string_of_term (back again from term.ML) -- should avoid this altogether;
2006-05-16 wenzelm 2006-05-16 more abstract interface to classes/arities;
2006-05-16 wenzelm 2006-05-16 replaced low-level Term.str_of by Display.raw_string_of_term (should actually use Display.string_of_term);
2006-05-16 wenzelm 2006-05-16 added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
2006-05-16 haftmann 2006-05-16 fixed handling of absolute urls
2006-05-15 urbanc 2006-05-15 added the lemmas pt_fresh_aux and pt_fresh_aux_ineq (they are used in the proof of the strong induction principle) added code to nominal_atoms to collect these lemmas in "fresh_aux" instantiated for each atom type deleted the fresh_fun_eqvt from nominal_atoms, since fresh_fun is not used anymore in the recursion combinator
2006-05-13 wenzelm 2006-05-13 reactivated translations for less/less_eq;
2006-05-13 wenzelm 2006-05-13 added add_primrec_unchecked_i;
2006-05-13 wenzelm 2006-05-13 unchecked definitions;
2006-05-13 wenzelm 2006-05-13 defs (unchecked overloaded), including former primrec; tuned;
2006-05-13 wenzelm 2006-05-13 updated;
2006-05-13 wenzelm 2006-05-13 add_defs: unchecked flag; tuned;
2006-05-13 wenzelm 2006-05-13 'defs': unchecked flag;
2006-05-13 wenzelm 2006-05-13 Theory.add_defs(_i): added unchecked flag;
2006-05-13 wenzelm 2006-05-13 added add_defs_unchecked(_i);
2006-05-13 wenzelm 2006-05-13 actually reject malformed defs; added unchecked flag; tuned;
2006-05-13 wenzelm 2006-05-13 moved defs explanation to isar-ref;
2006-05-13 wenzelm 2006-05-13 added defs (unchecked)''; more explanations on well-formednes of defs;
2006-05-13 wenzelm 2006-05-13 * Pure: overloaded definitions are now actually checked for acyclic dependencies;
2006-05-12 wenzelm 2006-05-12 tuned;
2006-05-12 nipkow 2006-05-12 added lemma in_measure
2006-05-12 haftmann 2006-05-12 fixed silly bug in function serializer for ML
2006-05-12 huffman 2006-05-12 add new finite chain theorems
2006-05-12 wenzelm 2006-05-12 improved propagate_deps; removed structs_less, which is actually unsound in conjunction with interdependent overloaded consts;
2006-05-11 wenzelm 2006-05-11 check result against certified prop, i.e. admit non-normal statements;
2006-05-11 wenzelm 2006-05-11 tuned;
2006-05-11 wenzelm 2006-05-11 avoid raw equality on type thm;
2006-05-11 wenzelm 2006-05-11 replaced Graph.fold_nodes by general Graph.fold;
2006-05-11 wenzelm 2006-05-11 added fold; removed fold_nodes; added IntGraph; tuned;
2006-05-11 wenzelm 2006-05-11 tuned Defs.merge;
2006-05-11 wenzelm 2006-05-11 allow dependencies of disjoint collections of instances; major cleanup;
2006-05-11 wenzelm 2006-05-11 use IntGraph from Pure;
2006-05-11 krauss 2006-05-11 Function Package: Quick-and-dirty-fixed strange "Proved a different theorem bug" due to abbreviations
2006-05-11 krauss 2006-05-11 Fix: Auto term must apply wf-intro rules repeatedly.
2006-05-11 haftmann 2006-05-11 fixed codegen bug, cleanup
2006-05-10 wenzelm 2006-05-10 revert accidental text change;
2006-05-09 haftmann 2006-05-09 introduced characters for code generator; some improved code lemmas for some list functions
2006-05-09 haftmann 2006-05-09 added .cvsignore
2006-05-09 haftmann 2006-05-09 added ExecutableRat.thy
2006-05-09 haftmann 2006-05-09 removed 1::int
2006-05-09 haftmann 2006-05-09 added preprocs for CodegenTheorems
2006-05-09 haftmann 2006-05-09 improved code generation for wfrec
2006-05-09 haftmann 2006-05-09 added codegen preprocessors for numerals
2006-05-09 haftmann 2006-05-09 adaption to CodegenTheorems
2006-05-09 haftmann 2006-05-09 added DatatypeHooks
2006-05-09 haftmann 2006-05-09 different object logic setup for CodegenTheorems
2006-05-09 haftmann 2006-05-09 major refinement of codegen_theorems.ML
2006-05-09 haftmann 2006-05-09 removed superfluous eq_ord
2006-05-09 haftmann 2006-05-09 improved chmod/chgrp handling
2006-05-08 huffman 2006-05-08 speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
2006-05-08 wenzelm 2006-05-08 quoted 'termination' command;
2006-05-08 wenzelm 2006-05-08 Defs.define: const_typargs;
2006-05-08 wenzelm 2006-05-08 added raw_string_of_sort/typ/term;
2006-05-08 wenzelm 2006-05-08 simple substructure test for typargs (independent type constructors);
2006-05-08 wenzelm 2006-05-08 tuned;
2006-05-08 webertj 2006-05-08 string_of_option tuned
2006-05-07 wenzelm 2006-05-07 * Isar: removed obsolete 'concl is' patterns.
2006-05-07 wenzelm 2006-05-07 removed 'concl is' pattern;