renamed body_context_node to presentation_context;

add_locale(_i): return actual result context; cert_facts: allow qualified names;

class(_i): mimic Locale.add_locale(_i); 'class': begin_local_theory;

added type global_theory -- theory or local_theory; added begin/exit_local_theory; removed theory_context; renamed body_context_node to presentation_context; removed copy (checkpoint twice instead -- avoids unrelated theories);

added begin;

added opt_begin;

added raw_theory(_result); tuned;

Toplevel.end_proof;

'end': handle local theory; 'locale': begin local theory;

undo_end/kill: handle local theory; Toplevel: generic_theory;

Toplevel: generic_theory;

made some proof look more like the ones in Barendregt

A way to call the ATP linkup from ML scripts

Combinators require the theory name; added settings for SPASS

stripped pointless head

gen_rem(s) abandoned in favour of remove / subtract

added IsarAdvanced material

Induction rules have schematic variables again.

initial draft

*** empty log message ***

initial draft

fixed intendation

cleanup basic HOL bootstrap

added legacy tactic

purged some ML legacy

added eq_True eq_False True_implies_equals to extraction_expand

no breaks for Haskell

removed experimental codegen_simtype

added keeping of funcgr

generalized purge

changed order

removed quote in serialization

added code_abstype

added code_constsubst

fixed typo

added code_abstype and code_constsubst

isabelle-process: options -S, -X;

tuned;

loop: disallow exit in secure mode;

Secure.commit;

moved Context.ml_output to Output.ml_output;

Secure critical operations.

added General/secure.ML;

added option -S (secure mode);

added nbe_post for delayed_if

added delayed_if

added pre/post-processor equations

attribute "symmetric": standardized schematic variables;

sequential lemmas;

reorderd ML/lemmas (Why!?);

PureThy.note_thmss_i;

added exit; notes: simplified locale target;

added theorems(_i) -- with present_results;

def(_i): LocalDefs.add_defs; removed Drule.strip_shyps_warning;

attribute: Context.mapping; removed Drule.strip_shyps_warning;

removed obsolete note_thmss(_i); simplified add_thmss; tuned;

added exit;

simplified derived_def;

removed theorems, smart_theorems etc. (cf. Specification.theorems);

lemmas/theorems/declare: Specification.theorems;

added kind attributes;

Drule.lhs/rhs_of;

added dest_equals_lhs; replaced clhs/crhs_of by lhs/rhs_of; local_standard: flexflex_unique; removed strip_shyps_warning;

attribute: Context.mapping; Proof.theorem_i;

replaced Drule.clhs/crhs_of by Drule.lhs/rhs_of;

attribute: Context.mapping; PureThy.note_thmss_i;

standardized facts;

attribute symmetric: zero_var_indexes; tuned proofs;

attribute symmetric: zero_var_indexes;

attribute: Context.mapping;

cleaned up interfaces

Removed unused res_atp_setup.ML, since its functions have been put in res_atp.ML.

Common theory targets.

Element.export_facts;

refined unlocalize_mixfix;

TheoryTarget;

moved pretty_consts to proof_display.ML; adapted to improved LocalTheory interfaces;

added pretty_consts (from specification.ML);

turned into abstract wrapper module, cf. theory_target.ML; simplified interfaces;

replaced add_def by more elaborate add_defs; added find_def (based on educated guesses);

replaced generalize_facts by full export_(standard_)facts;

Thm.def_name_optional; ProofDisplay.pretty_consts;

added def_name_optional;

removed is_equals, is_implies; tuned;

added the_single;

added term_rule;

added Isar/theory_target.ML;

improved LocalDefs.add_def;

mk_partial_rules_mutual: expand result terms/thms;

removed with_local_path -- LocalTheory.note admits qualified names; TheoryTarget.init;

moved the_single to Pure/library.ML; tuned;

TheoryTarget.init;

tuned comments;

tuned method syntax: polymorhic term argument; tuned rule instantiation;

tuned;

Fixed the printing of the used theorems by maintaining separate lists for each subgoal. Retains the ATP input files if debugging is on.

Tidied code to delete tmp files. Fixed the printing of the used theorems by maintaining separate lists for each subgoal.

renamed the combinator laws

Improved detection of identical clauses, also in the conjecture

Refinements to abstraction. Seeding with combinators K, I and B.

examples for hex and bin numerals

Changed and removed some functions related to combinators, since they are Isabelle constants now.

Now the DFG output includes correct declarations of c_fequal, but not hEXTENT

improvements to abstraction, ensuring more re-use of abstraction functions moving some functions to Pure/drule.ML

facts about combinators

a few new functions on thms and cterms

reorganize and speed up termdiffs proofs

fixed bug in linear arith

improvements for Haskell serialization

insert replacing ins ins_int ins_string

cleaned up some mess

clarified header comments

insert replacing ins ins_int ins_string

*** empty log message ***

tuned

Improved error reporting

nnf_simpset built statically

rewrite proofs of powser_insidea and termdiffs_aux

generalize summability lemmas using class banach

clarified setup name

various code refinements

fixed some Haskell issues

changed preprocessing framework

clarified some things

cleaned and extended

added gen_primrec

added code for insert

improvements for code_gen

cleaned mess

added example for code_gen

dropped obsolete Theory.sign_of

tuned

added code generator names for nat_rec and nat_case

improved serialization for arbitrary

normal_form now a diagnostic command

restructured contents

add axclass banach for complete normed vector spaces

remove unused Cauchy_Bseq lemmas

add lemmas norm_not_less_zero, norm_le_zero_iff

added is_Trueprop

tidying and simplifying

Changing the default for theory_const

extensions for Susanto

restored the "length of name > 2" check for package definitions

Now checks explicitly for Trueprop, thereby ignoring junk theorems involving OF_CLASS, etc.

exists_name: include this theory name;

removed obsolete Datatype_Universe.thy (cf. Datatype.thy);

merged with theory Datatype_Universe;

obsolete;

renamed ex/SVC_Oracle.ML to ex/svc_oracle.ML;

removed share_data; tuned;

cterm_match: avoid recalculation of maxidx;

reverted to revision 1.28;

proper use of svc_oracle.ML;

reactivated theory PER; removed obsolete StringEx;

tuned proofs;

moved theory Infinite_Set to Library; tuned proofs;

moved theory Infinite_Set to Library;

moved Infinite_Set.thy to Library; removed obsolete ex/StringEx.thy; renamed ex/SVC_Oracle.ML to ex/svc_oracle.ML;

tuned;

Removed the helper files (combinator rewrite rules, function extensionality and fequal rules).

generalize more DERIV proofs

statement: Variable.fix_frees;

added undo_end;

tuned proofs;

proper import of Main HOL;

tuned specifications and proofs;

hides popular names (from Datatype.thy);

removed obsolete sum_case_Inl/Inr; moved 'hide' to Datatype_Universe; tuned proofs;

renamed Variable.invent_fixes to Variable.variant_fixes;

generalize proofs of DERIV_isCont and DERIV_mult

generalized some DERIV proofs

add scaleR lemmas

generalize type of DERIV

add type annotations for DERIV

Combinator axioms are now from Isabelle theorems, no need to use helper files. Removed LAM2COMB exception.

Added the combinator constants to the constants table.

Removed ResHolClause.LAM2COMB exception.

Reordered how files are loaded.

moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;

removed mixfix_content;

Syntax.mode; refrain from removing conflicting mixfixes;

Syntax.mode;

Sign.add_consts_authentic;

proper use of matrixlp.ML;

simplified is_package_def -- be less ambitious about B library operations;

obsolete;

added share_data;

Sign.add_consts_authentic;

consts: syntax consts only for actual syntax;

added share_data (dummy);

removed obsolete HOLCF.ML;

ResAtpset.get_atpset;

removed legacy code; tuned;

tuned definitions/proofs;

proper use of float.ML;

fixed translations: CONST;

replaced syntax/translations by abbreviation; fixed translations: CONST;

replaced syntax/translations by abbreviation;

removed obsolete Real/document/root.tex; removed obsolete Isar_examples/Cantor.ML; renamed Real/Float.ML to Real/float.ML;

tuned;

rearranged axioms and simp rules for scaleR

added Poly/ML 4.9.1 (experimental!);

rearranged axioms and simp rules for scaleR

clearout of obsolete code

addition of combinators

tuned messages;

tuned;

LD_LIBRARY_PATH;

Definitions produced by packages are now blacklisted.

more reorganizing sections

reorganize sections

add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer

add lemma hypreal_epsilon_gt_zero

generalize type of is(NS)UCont

add intro/dest rules for (NS)LIMSEQ and (NS)Cauchy; rewrite equivalence proofs using transfer

proper use of PolyML.shareCommonData;

add lemmas InfinitesimalI2, InfinitesimalD2

adapted to pre-5.0 versions;

Poly/ML startup script (for 4.9.1);

added ML-Systems/polyml-4.9.1.ML;

Compatibility wrapper for Poly/ML 4.9.1.

removed all references to star_n and FreeUltrafilterNat

add lemmas about hnorm, Infinitesimal

reverted to 1.58;

proper const_syntax for uminus, abs;

reorganized HNatInfinite proofs; simplified and renamed some lemmas

removed obsolete of_instream_slurp -- now already included in tty;

Source.tty now slurps by default;

of_stream/tty: slurp input eagerly;

tuned all_paths;

internal params: Vartab instead of AList;

removed unused serial_of, name_of;

removed redundant lemmas;

remove redundant lemmas

replaced constant 0 by HOL.zero

hypreal_of_nat abbreviates of_nat

add lemmas of_real_eq_star_of, Reals_eq_Standard

move star_of_norm from SEQ.thy to NSA.thy

convert more proofs to transfer principle

add lemmas about Standard, real_of, scaleR

instance complex :: real_normed_field; cleaned up

add lemma stc_unique; shorten stc proofs

add lemmas approx_diff and st_unique, shorten st proofs

add lemmas about of_real and power

reorganize section headings

more lemmas about Standard and star_of

define new constant Standard = range star_of

add lemmas of_int_in_Reals, of_nat_in_Reals

add header

Changed precedence of "op O" (relation composition) from 60 to 75.

handling of \<^const> syntax for case; explicit case names for induction rules for rep_datatype

tuned syntax for <= <

renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes

renamed 0 and 1 to HOL.zero and HOL.one respectivly

fixed the definition of "depth"

Abstraction now handles equations where the RHS is a lambda-expression; also, strings of lambdas

some cleanup

changed order

inserted headings

changed interface in codegen_package.ML

fixed some mess

cleaned up

adding constants the modern way

added examples for variable name handling

better handling for div by zero

updated theory description

refinements in codegen serializer

added 'undefined' serializer

added code_instname

reorganized subsection headings

moved SEQ_Infinitesimal from SEQ to HyperNat

real_norm_def [simp]

generalize types of lim and nslim

generalized types of sums, summable, and suminf

add lemma convergent_Cauchy

remove extra dependencies

add proof of summable_LIMSEQ_zero

change definitions from SOME to THE

move root and sqrt stuff from Transcendental to NthRoot

fix proof

added lemmas about LIMSEQ and norm; simplified some proofs

add lemma norm_power

added HOL-Complex-ex;

define constants with THE instead of SOME

Fixed bug concerning the generation of identifiers for datatypes, which caused the code generator to fail for mutually recursive datatypes.

Replaced irreducible_paths by all_paths.

Added function all_paths (formerly find_paths).

tuned proofs;

tuned oracle name;

added is_ml_reserved;

member (op =); tuned;

serial numbers for types;

added dest_binop;

member (op =); tuned pattern check;

member (op =); Drule.dest_equals_rhs;

tuned eta_contract;

added dest_equals_rhs; moved dest_binop to thm.ML;

tuned;

serial numbers for consts; added serial_of/name_of;

Thm.dest_binop;

member (op =); ThmDatabase.is_ml_reserved; tuned oracle name;

member (op =);

updated timings;

new function hashw_int

Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions unless theorems differ by sorts alone, which should not matter. Also minor fixes to standard hashing.

corrected for the translation from _ to __ in c_COMBx_e

changed constants into abbreviations; shortened proofs

XML syntax for types, terms, and proofs.

Added xml_syntax.ML

Added Tools/xml_syntax.ML

circumvented defect in SML/NJ type inference

1. Function package accepts a parameter (default "some_term"), which specifies the functions behaviour outside its domain. 2. Bugfix: An exception occured when a function in a mutual definition was declared but no equation was given.

removed division_by_zero class requirements from several lemmas

added approx_hnorm theorem; removed division_by_zero class requirements from several lemmas

choose gnuplot terminal by platform

set terminal png color -- works for older versions of gnuplot;

added ZF-UNITY;

tidied

Added in combinator reduction axioms for B' C' and S'. Also split the original reduction axioms into separate files: I+K, B+C, S, B'+C', S'.

make it work on sunbroy2

Moved the functional equality axioms to helper1 files.

Introduced combinators B', C' and S'.

Removed include_min_comb and include_combS.

Add Source.of_instream_slurp to try to ensure that XML parser sees whole documents.

improvements for codegen 2

name shifts

fixed bug

Removed "induct set" attribute from total induction rules

removed debug

Fixed error in pattern splitting algorithm

change section to subsection

add header

renamed axclass_xxxx axclasses;

tuned;

added standard;

added name_classrel/arities/arity;

pretty_full_theory: suppress internal entities by default;

Logic.name_classrel/arities;

revert to previous version;

added General/susp.ML;

removed duplicate arities;

sko/abs: Name.internal prevents choking of print_theory;

tuned method setup;

tuned proofs;

'print_theory': bang option for full verbosity;

* Pure: 'print_theory' now suppresses entities with internal name;

tuned;

simple html output;

timespan: 100 days;

superceded by isatest-statistics;

tuned;

target dir; proper time formats;

Standard statistics.

time: include year;

Produce statistics from isatest session logs.

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);