Major update to function package, including new syntax and the (only theoretical) ability to handle local contexts.

added instance rat :: recpower

more on theorems;

tuned;

more on terms;

no_syntax norm -- clash with Real/RealVector.thy;

simplify some proofs, remove obsolete realpow_divide

realpow_divide -> power_divide

remove extra dependency

more on terms; tuned;

Efficient term substitution -- avoids copying. moved here from term.ML; added instantiate_maxidx;

ctyp: maintain maxidx; cterm_match: tight maxidx for substitution; instantiate: determine maxidx from insts -- major performance improvement; moved term subst functions to TermSubst; tuned;

removed obsolete aconvs (use eq_list aconv); tuned aconv --- more efficient on identical subterms; moved term subst functions to term_subst.ML;

tuned eq_list;

moved term subst functions to TermSubst;

intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;

added Pure/term_subst.ML;

added Gentzen:1935;

import RealVector

formalization of vector spaces and algebras over the real numbers

induct method: renamed 'fixing' to 'arbitrary';

updated;

more rules;

hid succ, pred in Numeral.thy

updated;

more rules;

tuned;

added axclass division_ring (like field without commutativity; includes e.g. quaternions) and generalized some theorems from field to division_ring

cleaned up

tuned;

tuned;

changed order of type classes and axclasses

tuned;

updated;

tentative appendix C;

tuned;

read_instantiate: declare names of TVars as well (temporary workaround for no-freeze feature of type inference);

rawsat_thm: mk_conjunction_list replaced by Conjunction.mk_conjunction_list

got rid of Numeral.bin type

now using TypecopyPackage

TypedefPackage.add_typedef_* now yields name of introduced type constructor

added Barendregt-Geuvers:2001;

updated;

more on types and type classes;

tuned;

added \isactrlvec;

tuned;

more on names;

tuned;

tuned;

Using Drule.local_standard to reduce the space usage

tuned;

updated;

more on variables; tuned;

More locale test code.

Documented methods intro_locales and unfold_locales.

some corrections in class section

explicit table with constant types

proper project_sort

tuned

zchaff_with_proofs: proof is a reference now

signature: do not export private stuff;

skolem_cache_thm: Drule.close_derivation on clauses preserves some space; tuned skolem_cache operations: canonical argument order; tuned monomorphic test;

tuned;

tuned;

explain assumptions;

refinements to conversion into clause form, esp for the HO case

pervasive refinements

removed some dictionary stuff

project_algebra yields sort projector

final syntax for some Isar code generator keywords

tuned;

misc cleanup;

tuned;

more stuff;

mldecls: footnotesize;

more on contexts;

String.concatWith (not available in PolyML) replaced by space_implode

improvements to abstraction generation

blacklist now handles thm lists

Empty is better than Match

term_of_prop_formula added

read_dimacs_cnf_file ignores more comment lines

faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses

code refinements

updated;

tuned;

added yet another code generator example

fixes

fixed bug in wfrec appgen

lin_arith_prover: splitting reverted because of performance loss

lin_arith_prover: splitting reverted because of performance loss

added a FIXME-comment

tuned;

more on contexts;

refinements

added and refined some exmples

added typecopy_package

added typecopy_package and some examples

updated keywords

minor bug fixes

removed the (apparently pointless) signature constraint

tidied

encode clauses as Isar premises, rather than as object-logic &, for faster parsing

abstraction of lambda-expressions

tidied

better skolemization, using first-order resolution rather than hoping for the right result

using inc

explicit type variables prevent empty sorts

replaced skolem declarations by automatic skolemization of everything

avoid duplicate tactics

additional list of tactics that can be added to arith

Added premises concerning finite support of recursion results to FCBs.

speed up proof of summable_Cauchy

speed up some proofs

generalize proof of SUP_rabs_subseq

speed up some proofs

SML/NJ int type fix

tracing

improved preprocessing

fixed bug in sortlookup

more concise preprocessing of numerals for code generation

more concise string serialization

added some codegen examples/applications

adapted using the characteristic equations

modified to use the characteristic equations

- Fixed bug that caused uniqueness proof for recursion combinator to fail for mutually recursive datatypes - Implemented proofs of characteristic equations for recursion combinator.

used the recursion combinator for the height and substitution function