classes: maintain serial number;

tuned;

isatool browser: renamed option -d to -c (cf. isatool tool)

PRIVATE_FILE: slightly more robust way to create and dispose;

renamed option -d to -c (cf. isatool display); operate on PRIVATE_FILE;

updated;

Bug fix to prevent exception dest_Free from escaping

Added the max_new parameter, which is a cap on how many clauses may be admitted per round. Also various tidying up.

replaced implodeable_Ext by set_like

Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n) instead of only ... = xs!n.

replace (x + - y) with (x - y)

add type constraint to otherwise looping iff rule

generalize type of (NS)LIM to work on functions with vector space domain types

norm_one is now proved from other class axioms

removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants

hcmod abbreviates hnorm :: hcomplex => hypreal

complex_of_real abbreviates of_real::real=>complex; cmod abbreviates norm::complex=>real; removed several redundant lemmas

add instance for real_algebra_1 and real_normed_div_algebra

add instances for real_vector and real_algebra

define new constant of_real for class real_algebra_1; define set Reals as range of_real; add lemmas about of_real and Reals

int_diff_cases moved to Integ/IntDef.thy

generalized types of many constants to work over arbitrary vector spaces; modified theorems using Rep_star to eliminate existential quantifiers

add theorem norm_diff_triangle_ineq

add required type annotation

removed type aliases for theory/theory_ref;

renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);

tuned;

rrule: maintain 'extra' field for rule that contain extra vars outside elhs; rewrite_rule_extra_vars: tuned; rewritec: omit incr_indexes in most cases, which is a big performance gain;

instantiate: omit has_duplicates check, which is irrelevant for soundness;

trivial whitespace change

tuned;

more on theorems;

generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space

add instance for class division_ring

removed duplicate lemmas

fixed syntax clash with Real/RealVector

*** empty log message ***

Function package: Outside their domain functions now return "arbitrary".

updated makefile

Fixed Subscript Exception occurring with Higher-Order recursion

remove conflicting norm syntax

made SML/NJ happy;

added exists_type;

renamed NameSpace.drop_base to NameSpace.qualifier;

Updated keyword file

Removed debugging code imports...

Added the "theory_const" option. Only it is OFF because it's often harmful!

Extended the blacklist with higher-order theorems. Restructured. Added checks to ensure that no higher-order clauses are output in first-order mode.

bug fix to abstractions: free variables in theorem can be abstracted over.

Tweaks to is_fol_term, the first-order test. We don't count "=" as a connective since this test is applied to clause forms.

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