removed

moved part of normalization oracle here

classical arity syntax

added codegen_data

moved base setup for evaluation oracle hier

added OperationalEquality.thy

code generation 2 adjustments

(void)

improved numeral handling for nbe

added suspensions in Pure

added some stuff for code generation 2

dropped error-prone code generation 2 for wfrec

text cleanup

introduced syntactic classes; moved some setup to Pure/codegen, Pure/nbe or OperationalEquality.thy

explicit divmod algorithm for code generation

added operational equality

added section on code generation 2

code_gen now peek keyword

cleanupdiff

added classes real_div_algebra and real_field; added lemmas

add Real/RealVector.thy

* Pure: 'class_deps' command visualizes the subclass relation;

added class_deps;

added dest_arg, i.e. a tuned version of #2 o dest_comb;

Thm.dest_arg;

Present.display_graph;

added display_graph (from thm_deps.ML);

output: uninterpreted raw symbols -- these are usually LaTeX macros;

pretty_thm: graceful treatment of ProtoPure.thy;

added class_deps;

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