moved Import/susp.ML to Pure/General;

renamed axclass_xxxx axclasses

removed diagnostic messages

Operational Equality

this file contains a compile-challenge suggested by Adam Chlipala; so far it contains only the definition and no proofs

tuned

added auxiliary lemma for code generation 2

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

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

added definition for size and substitution using the recursion combinator

improved thmtab

fixed bug in sortcontext extraction

dropped definitions_of

added all_super_classes

renamed module to thyname

cleanup

added missing supp_nat lemma

added

module restructuring

code cleanup, instance_subsort now working

added code generator packages

adaptions to improvements

added add_hook_bootstrap

added new files

simplified code generator setup

added passage on class package

updated code generator keywords

Removed non-trivial definitions from calc_atm theorem list.

Finished implementation of uniqueness proof for recursion combinator.

*** empty log message ***

Reification now handels binders.

consistent prefixing for skolem functions

blacklist augmented to block some "unit" theorems that cause unsound resolution proofs

tuned: string_of_list, string_of_pair