added Tools/nbe, fixes

added Tools/nbe

New normalization-by-evaluation package

distinct (op =); removed spurious PolyML.print;

fixed

Inclusion of subset_refl in ATP calls

Fix variable-naming bug (?) by removing a needless recursive call

slight code generator serialization improvements

moved intro_classes from AxClass to ClassPackage

fixed document

* denumerability of rationals by Benjamin Porter, based on NatPair (by Stefan Richter) #3 in http://www.cs.ru.nl/~freek/100/

added a few lemmas to do with permutation-equivalence for the recursion combinator

* added Library/ASeries (sum of arithmetic series with instantiation to nat and int) * added Complex/ex/ASeries_Complex (instantiation of the above for reals) * added Complex/ex/HarmonicSeries (should really be in something like Complex/Library) (these are contributions by Benjamin Porter, numbers 68 and 34 of http://www.cs.ru.nl/~freek/100/)

use minimal imports

use qualified name for return

dest_def: tuned error msg;

const constraints: provide TFrees instead of TVars, actually delete constraint (allows Consts.merge caused by ProofContext.transfer after qed);

checkpoint/copy_node: reset body context;

global_qeds: transfer body context;

add_const_constraint(_i): demand TFrees instead of TVars, optional type (i.e. may delete constraints);

constrain: assert const declaration, optional type (i.e. may delete constraints);

removed Import/lazy_scan.ML;

hyperlinks in the PDF work now

replaced Symbol.explode by explode

updated mailing list archive link

use monomorphic sequences / scanners

make maybe into a real type constructor; remove monad syntax

use VectorScannerSeq instead of ListScannerSeq in xml.ML

removed lazy_scan

improved scanning

tuned;

Abstract Natural Numbers with polymorphic recursion.

new-style definitions/abbreviations;

added ex/Abstract_NAT.thy;

tuned;

tuned;

removed silly stuff

* Isar/locales: new derived specification elements 'definition', 'abbreviation', 'axiomatization';

added abbreviation(_i);

added put_thms_internal: local_naming, no fact index; tuned;

added put_thms_internal; tuned;

added abbrev element;

added 'abbreviation'; tuned;

added premsN;

Proof.put_thms_internal;

removed pointless replace;

tuned;

dest_def: actually return beta-eta contracted equation;

derived specifications: definition, abbreviation, axiomatization;

updated;

cache improvements

variable counter is now also cached

adapted to kernel changes

tuned subst_bound(s);

fixed bugs, added caching

added cases_node; replaced body_context_of by body_context_node, removed no_body_context; copy: ProofContext.transfer; added present_local_theory, present_proof; removed internal command interface;

replaced qualified_force_prefix to sticky_prefix; do not export read_terms;

removed distinct, renamed gen_distinct to distinct; replaced qualified_force_prefix by qualified_names/sticky_prefix;

check_text: Toplevel.node option;

init/exit no longer change the theory (no naming); added naming, restore_naming, mapping;

evaluate antiquotes depending on Toplevel.node option;

simplified presentation commands;

sane version of distinct_subgoals_tac, based on composition with Drule.distinct_prems_rl;

removed qualified_force_prefix; added sticky_prefix;

replaced qualified_force_prefix to sticky_prefix;

chop is no longer pervasive; removed obsolete thms_containing;

rewrite_cterm: Thm.adjust_maxidx prevents unnecessary increments on rules;

added distinct_prems_rl;

specifications_of: avoid partiality;

counter example: avoid vacuous trace;

cannot use section before setup;

used Tactic.distinct_subgoals_tac;

removed distinct, renamed gen_distinct to distinct;

added lemma pt_perm_compose'

got rid of superfluous linorder_neqE-instance for int.

typo in a comment fixed

exported some interfaces useful for other code generator approaches

some fixes

exported specifications_of

added theory of executable rational numbers

improved handling of iml abstractions

fixed tracing

Adapted to Context.generic syntax.

Fixed a bug of type unification.

* ML/Pure/General: improved join interface for tables;

consts: maintain thy version for efficient transfer; ins_sorts: Vartab.replace is slower than Vartab.update, but might avoid some copying of table structure;

tuned;

export exception SAME (for join); join: use internal modify, no option type (handle SAME/DUP instead); defined: simplified copy of lookup code, avoids allocation of option constructor; added replace, which does not change equal entries;

low-level tuning of merge: maintain identity of accesses; simplified TableFun.join;

share exception UNDEF with Table; simplified TableFun.join;

structure Datatab: private copy avoids potential conflict of table exceptions; simplified TableFun.join;

added eq_consts; reverted abbrevs: try all abstraction prefixes;

minor tuning of proofs, notably induct;

simplified TableFun.join;

\usepackage{amssymb};

* include generalised MVT in HyperReal (contributed by Benjamin Porter) * add non-denumerability of continuum in Real, includes closed intervals on real (contributed by Benjamin Porter, #22 in http://www.cs.ru.nl/~freek/100/)

* moved ThreeDivides from Isar_examples to better suited HOL/ex * moved 2 summation lemmas from ThreeDivides to SetInterval

divisibility by 3 theorem, contributed by Benjamin Porter, #85 in http://www.cs.ru.nl/~freek/100/

replaced mixfix_conflict by mixfix_content;

added map_theory; added rename_frees; removed custom_accesses; added qualified_force_prefix; tuned local syntax;

added abbreviations: activated by init, no expressions yet;

added restore; consts: provide abbreviations;

tuned mixfixes, mixfix_conflict;

removed custom_accesses; added suffixes_prefixes_split, qualified_force_prefix;

added variant_name;

removed custom_accesses; added qualified_force_prefix;

tuned;

added chop (sane version of splitAt); added prefixes, suffixes;

Changed some code due to changes in reduce_axiomsN.ML.

Added another filter strategy.

improved code generator devarification

statement: improved error msg;

* ML/Pure: generic Args/Attrib syntax everywhere;

moved fixedN to lexicon.ML; tuned;

added mfix_delims; tuned;

added mixfix_conflict;

added fixedN, constN;

tuned comment; moved local syntax to local_syntax.ML; common naming (for abbrevs and thms); transfer: merge consts; tuned pretty_term'; added polymorphic -- special case of generalize; added add_abbrevs(_i); read/cert: expand_consts;

tuned comment;

syntax: Context.generic;