Adapted to changes in FixedPoint theory.

method exported

updated NEWS

* 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.

added gfx

dropped blastdata.ML

(adjustions)

two further lemmas on split

removed dependency of ord on eq

removed itrev as inlining theorem

added state monad to HOL library

code generator module naming improved

(continued)

(continued)

minor cleanup

case_tr: do not intern already internal consts;

updated;

removed isactrlconst;

instantiate: avoid global references;

added const_syntax_name;

removed obsolete first_duplicate;

added syntax_name;

fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;

Sign.const_syntax_name;

added gfx

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;

String.compare: slow version -- performance test;

replaced apply_copy by apply'; tuned;

removed is_Trueprop (use can dest_Trueprop'' instead);

removed is_Trueprop (use can dest_Trueprop'' instead); tuned list_all;

updated;

HOL_USEDIR_OPTIONS: -p 1 by default;

tuned;

* October 2006: Stefan Hohe, TUM;

replaced Toplevel.proof_to_theory by Toplevel.end_proof;

optional argument for timespan (default 100);

added at-mac-poly-e, at64-poly-e;

moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs

new Deriv.thy contains stuff from Lim.thy

re-added simpdata.ML

new ML serializer

fixed problem with eta-expansion

tuned

fixed problem with variable names

tightened notion of function equations

dropped name_mangler.ML

some example tweaking

added particular test for partially applied case constants

improved evaluation setup

adapted to changes in codegen_data.ML

added code gen II

simplified reasoning tools setup

dropped prop_cs

dropped equals_conv for nbe

first version of style guide

continued tutorial

added serialization keywords

bugfix to zipto: left and right were wrong way around.

added sum_squared

changed a misplaced "also" to a "moreover" (caused a loop somehow)

changed to not compile Iteration and Recursion, but Lam_Funs instead

move DERIV_sumr from Series.thy to Lim.thy

generalize type of lemma isCont_Id

new proof of Bseq_NSbseq using transfer

changed to use Lam_Funs

clauses for iff-introduction, unfortunately useless

tuned

Numerous cosmetic changes. Use of ---> notation for types. Added rules for the introduction of the iff connective, but they are too prolific to be useful.

not needed anymore

these files are superseded by the internal recursion combinator and the file Lam_Funs.thy

More blacklisting CASC mode now always on, due to switch to Vampire 8.1 (i.e. the 2006 version) Now runs ATPs unless time_limit = 0.

added lexicographic_order tactic

new SML serializer

clarified make_term interface

introduced CodegenData.add_func_legacy

cleaned up

adapted seralizer syntax

adapted to new serializer syntax

constructing proof

dropped constructiv `->

new serialization syntax; experimental extensions

refined

refined algorithm

simplified preprocessor framework

cleanup

*** empty log message ***

fixed type signature of Type.varify

dropped junk

disabled some code generation (an intermeidate solution)

adapted to new serializer syntax

added Equals_conv

cleaned up

adaptions to changes in preprocessor

dropped nth_update

Purely cosmetic

new file for defining functions in the lambda-calculus

Added "recdef_wf" and "simp" attribute to "wf_measures"

Removed debugging output

removed free "x" from termination goal...

Added "measures" combinator for lexicographic combinations of multiple measures.

Conversion to clause form now tolerates Boolean variables without looping. Attribute "clausify" moved to res_axioms; rest of reconstruction.ML deleted

adapted to Stefan's new inductive package

Fixed bug in the handling of congruence rules

(added entry)

switched merge_alists'' to AList.merge'' whenever appropriate

new single-step proofs

meson method MUST NOT use all safe rules, only basic ones for the logical connectives.

Improved tracing

fixed two bugs

bugfixes

added example with split

cleanup in ML setup code

added option of Haskell serializer

continued

Added freshness context to FCBs.

Adapted to changes in FCBs.

Added Compile and Height examples.

Added Compile and Height examples to Nominal directory.

removed antisym_setup.ML

cleaned up