2006-11-07 krauss 2006-11-07 Preparations for making "lexicographic_order" part of "fun"
2006-11-07 wenzelm 2006-11-07 renamed 'const_syntax' to 'notation';
2006-11-07 wenzelm 2006-11-07 'const_syntax' command: allow fixed variables, renamed to 'notation';
2006-11-07 wenzelm 2006-11-07 replaced const_syntax by notation, which operates on terms; read_const: include type;
2006-11-07 wenzelm 2006-11-07 Isar.context: proper error;
2006-11-07 wenzelm 2006-11-07 replaced const_syntax by notation, which operates on terms;
2006-11-07 wenzelm 2006-11-07 read_const: include type;
2006-11-07 wenzelm 2006-11-07 renamed 'const_syntax' to 'notation'; proper notation for fixed variables;
2006-11-07 wenzelm 2006-11-07 updated;
2006-11-07 berghofe 2006-11-07 Adapted to changes in FixedPoint theory.
2006-11-07 krauss 2006-11-07 method exported
2006-11-07 krauss 2006-11-07 updated NEWS
2006-11-07 krauss 2006-11-07 * Added annihilation axioms ("x * 0 = 0") to axclass semiring_0. Richer structures do not inherit from semiring_0 anymore, because anihilation is a theorem there, not an axiom. * Generalized axclass "recpower" to arbitrary monoid, not just commutative semirings.
2006-11-07 haftmann 2006-11-07 added gfx
2006-11-06 haftmann 2006-11-06 dropped blastdata.ML
2006-11-06 haftmann 2006-11-06 (adjustions)
2006-11-06 haftmann 2006-11-06 two further lemmas on split
2006-11-06 haftmann 2006-11-06 removed dependency of ord on eq
2006-11-06 haftmann 2006-11-06 removed itrev as inlining theorem
2006-11-06 haftmann 2006-11-06 added state monad to HOL library
2006-11-06 haftmann 2006-11-06 code generator module naming improved
2006-11-06 haftmann 2006-11-06 (continued)
2006-11-06 haftmann 2006-11-06 (continued)
2006-11-06 krauss 2006-11-06 minor cleanup
2006-11-05 wenzelm 2006-11-05 case_tr: do not intern already internal consts;
2006-11-05 wenzelm 2006-11-05 updated;
2006-11-05 wenzelm 2006-11-05 removed isactrlconst;
2006-11-05 wenzelm 2006-11-05 instantiate: avoid global references;
2006-11-05 wenzelm 2006-11-05 added const_syntax_name;
2006-11-05 wenzelm 2006-11-05 removed obsolete first_duplicate;
2006-11-05 wenzelm 2006-11-05 added syntax_name;
2006-11-05 wenzelm 2006-11-05 fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
2006-11-05 wenzelm 2006-11-05 Sign.const_syntax_name;
2006-11-05 haftmann 2006-11-05 added gfx
2006-11-04 wenzelm 2006-11-04 removed checkpoint interface; moved back to copy/checkpoint instead of checkpoint/checkpoint (NB 1: checkpoint is idempotent, i.e. impure data is being shared, which is inappropriate; NB 2: copying a checkpoint always produces a related theory); present_proof: proper treatment of history; tuned;
2006-11-04 wenzelm 2006-11-04 String.compare: slow version -- performance test;
2006-11-04 wenzelm 2006-11-04 replaced apply_copy by apply'; tuned;
2006-11-04 wenzelm 2006-11-04 removed is_Trueprop (use can dest_Trueprop'' instead);
2006-11-04 wenzelm 2006-11-04 removed is_Trueprop (use can dest_Trueprop'' instead); tuned list_all;
2006-11-04 wenzelm 2006-11-04 updated;
2006-11-04 wenzelm 2006-11-04 HOL_USEDIR_OPTIONS: -p 1 by default;
2006-11-04 wenzelm 2006-11-04 tuned;
2006-11-04 wenzelm 2006-11-04 * October 2006: Stefan Hohe, TUM;
2006-11-04 wenzelm 2006-11-04 replaced Toplevel.proof_to_theory by Toplevel.end_proof;
2006-11-04 wenzelm 2006-11-04 optional argument for timespan (default 100);
2006-11-04 wenzelm 2006-11-04 added at-mac-poly-e, at64-poly-e;
2006-11-04 huffman 2006-11-04 moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
2006-11-04 huffman 2006-11-04 new Deriv.thy contains stuff from Lim.thy
2006-11-03 haftmann 2006-11-03 re-added simpdata.ML
2006-11-03 haftmann 2006-11-03 new ML serializer
2006-11-03 haftmann 2006-11-03 fixed problem with eta-expansion
2006-11-03 haftmann 2006-11-03 tuned
2006-11-03 haftmann 2006-11-03 fixed problem with variable names
2006-11-03 haftmann 2006-11-03 tightened notion of function equations
2006-11-03 haftmann 2006-11-03 dropped name_mangler.ML
2006-11-03 haftmann 2006-11-03 some example tweaking
2006-11-03 haftmann 2006-11-03 added particular test for partially applied case constants
2006-11-03 haftmann 2006-11-03 improved evaluation setup
2006-11-03 haftmann 2006-11-03 adapted to changes in codegen_data.ML
2006-11-03 haftmann 2006-11-03 added code gen II