added print_stmts;

added pretty_statement;

added command, keyword; added chunks2;

Output.add_mode: keyword component;

string_of_mixfix;

print_statement;

added remove_trrules(_i); tuned;

added is_elim (from Provers/classical.ML);

added 'no_translations';

added pretty_stmt; tuned;

declared_const: check for type constraint only, i.e. admit abbreviations as well; added del_trrules(_i);

ObjectLogic.is_elim;

tuned constdecl; added 'no_translations';

updated;

Pure: no_translations;

refined representation of instance dictionaries

entry for Library/AssocList

First version of function for defining graph of iteration combinator.

got rid of type Sign.sg;

renamed plus to add;

renamed const minus to subtract;

simplified AxClass interfaces;

added axclass_instance_XXX (from axclass.ML); Sign.read/cert_arity;

*** empty log message ***

added read_class, read/cert_classrel/arity (from axclass.ML);

moved read_class, read/cert_classrel/arity to sign.ML; axclass: moved outer syntax to isar_syn.ML; instance: moved to Tools/class_package.ML; simplified interfaces; tuned;

use axclass.ML earlier (in Isar/ROOT.ML);

nbe: no_document;

tuned;

exporting reapAll and killChild

text delimiter fixed

comment delimiter fixed

clauses now use (meta-)hyps instead of (meta-)implications; significant speedup

fix for document preparation

Added Library/AssocList.thy

renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.

Changed some warnings to debug messages

Frequency analysis of constants (with types). Ability to restrict the number of accepted clauses.

Shortened the exception messages from assume.

METAHYPS catches THM assume exception and prints out the terms containing schematic vars.

added many simple lemmas

Added more functions to the signature and tidied up some functions.

tuned;

tuned some proofs

select_goals: split original conjunctions;

method: goal restriction defaults to [1];

infer_derivs: avoid allocating empty MinProof;

tuned;

Isar/method: goal restriction;

constdecl: always allow 'where';

deleted some proofs "on comment"

tuned some proofs

tuned some of the proofs about fresh_fun

first running version of type classes

first running version of type classes

first running version of type classes

Frequency strategy. Revised indentation, etc.

*** empty log message ***

added ROOT.ML

Indentation

Tidying and restructuring.

Tidying and tracing. Handling exn CLAUSE so that errors don't reach top-level.

Tidying. clausify_rules_pairs_abs now returns clauses in the same order as before. Removal of the unused err_list.

Tidying. New invoke_atp_ml for top-level debugging. Flag to force FOL mode.

Tidying, and getting rid of SELECT_GOAL (as it does something different now)

Added HOL-ZF to Isabelle.

substantial improvement in codegen iml

Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset. The hash table (for removing duplicate) now stores clauses as Term.term with names.

relevance_filter takes input axioms as Term.term.

Proof reconstruction now only takes names of theorems as input.

Added tptp_write_file to write all necessary ATP input clauses to one file.

tptp_write_file now takes goals and axioms as Term.term and writes them to a file.

Added functions to retrieve local and global atpset rules. cnf thms to Term.term format.

Moved the settings for ATP time limit to res_atp.ML

Merged res_atp_setup.ML into res_atp.ML. HOL translation is integrated with background Isabelle-ATP linkup. Both ATP methods and background linkup retrieve lemmas stored in claset, simpset and atpset.

When ATP methods call ATPs, all input clauses from one subgoal are written to one file.

Merged res_atp_setup.ML into res_atp.ML.

SELECT_GOAL: fixed trivial case;

fixed a typo in a comment

tuned;

method: SelectGoals;

method: syntax for SelectGoals;

text: added SelectGoals;

tuned conj_curry;

added extract, retrofit;

added mk_conjunction; tuned conj_curry;

method: restriction to first n sub-goals;

minor changes

more examples

changed and retracted change of location of code lemmas.

ignore repeated vars on lhs, cleanup

improvements for nbe

reformatting

subset_refl now included using the atp attribute

moved the "use" directive

fixed the bugs itroduced by the previous commit

made some small changes to generate nicer latex-output

split the files - Iteration.thy contains the big proof of the iteration combinator - Recursion.thy derives from Iteration the recursion combinator - lam_substs.thy contains the examples (size, substitution and parallel substitution)

Added in a signature.

fixed a problem where a permutation is not analysed when the term is of the form (pi o f) x1...xn This was the case because the head of this term is the constant "nominal.perm". Now an applicability predicate decides the right behaviour of the simproc

streamlined the proof

refined representation of codegen intermediate language

some small tunings

added fresh_fun_eqvt theorem to the theorem collection

added initialisation-code for finite_guess

made some small tunings in the decision-procedure (in the order how the "small" tactics are called)

Added setup for "atpset" (a rule set for ATPs).

Added file Tools/res_atpset.ML.

Merged HOL and FOL clauses and combined some functions.

A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.

some minor tuning on the proofs

initial commit (especially 2nd half needs to be cleaned up)

removal of theory blacklist

new order for arity clauses

fixed but in freeze_spec

splitting up METAHYPS into smaller functions

typos

added a finite_guess tactic, which solves automatically finite-support goals

class package and codegen refinements

added nbe

added temp. nbe test

added nbe, updated neb_*

added nbe

Typo.

added support for arbitrary atoms in the simproc

put_thms: do_index;

rewrite_goals_rule_aux: actually use prems if present;

add_local: do_index;

replaced the lemma at_two by at_different; this lemma now proves EX b. a != b

improved the decision-procedure for permutations; now uses a simproc FIXME: the simproc still needs to be adapted for arbitrary atom types

improved codegen bootstrap

change in codegen syntax

some refinements

added more detailed data to consts

Reverted to old interface of AxClass.add_inst_arity(_i)

Adapted to Florian's recent changes to the AxClass package.

added lemmas at_two: EX a b in an atom type such that a !=b at_ds10 and a "test"-lemma at_prm_eq_compose (can probably be removed)

make SML/NJ happy;

Default type level is T_FULL now.

eprover removes tmp files too.

vampire/eprover methods can now be applied repeatedly until they fail.

removed obsolete meta_conjunction_tr';

rew: handle conjunctionI/D1/D2;

simplified Pure conjunction, based on actual const;

removed rename_indexes_wrt; added rename_indexes2; simplified Pure conjunction, based on actual const;

renamed class_axms to class_intros;

tuned proofs;

simplified Pure conjunction;

not_equal: replaced syntax translation by abbreviation; simplified Pure conjunction;

abandoned merge_alists' in favour of generic AList.merge

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;