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;

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;

Context.generic is canonical state of parsers; removed obsolete global/local parsers; tuned interfaces;

Local syntax depending on theory syntax.

decode: observe Syntax.constN;

removed obsolete add_typ/term_classes/tycons;

tuned extern_term, pretty_term';

removed set quick_and_dirty and ThmDeps.enable -- no effect here;

abbrevs: store in reverted orientation; tuned;

use proof_general.ML: setmp quick_and_dirty captures default value;

added Isar/local_syntax.ML;

tuned;

Args/Attrib syntax: Context.generic;

simplified polyml example;

tidying

blacklist tweaks

names for simprules

removed redundant lemmas

no longer need All_equiv lemmas

map_type_tvar/tfree: map_atyps;

tuned;

*** empty log message ***

made "dvd" on numbers executable by simp.

introduced gen_distinct in place of distinct

fixed the most silly bug conceivable in map_atyps

lambda: base name of Const;

adapted Sign.infer_types; removed obsolete lambda' -- same as Term.lambda;

has_duplicates;

adapted Sign.infer_types;

added local consts component; tuned;

Library.is_equal;

removed obsolete sign_of_cterm; adapted Sign.certify_term;

adapted Sign.infer_types(_simult), Sign.certify_term/prop;

export consts_of; removed const_expansion; pretty_term', infer_types(_simult): separate Consts.T argument; added generic certify; simplified certify_term/prop;

removed eq-polymorphic duplicates; renamed gen_duplicates to duplicates; added is_equal;

renamed space to space_of; removed expansion; added abbrevs_of; added read_const; certify: substitute arguments into expanded const; tuned;

renamed gen_duplicates to duplicates;

slight improvements in code generation

updated;

Logic.combound;

adapted Consts.dest;

Sign.cert_def; tuned;

added bound_vars;

TableFun: renamed xxx_multi to xxx_list; tuned;

Envir.(beta_)eta_contract; TableFun: renamed xxx_multi to xxx_list;

added local_theory, with optional locale xname;

type local_theory; removed _loc versions;

norm_term: Sign.const_expansion, Envir.expand_atom;

TableFun: renamed xxx_multi to xxx_list; tuned LocalDefs.cert_def;

type local_theory = Proof.context; print_consts: subject to quiet_mode;

cert_def: use Logic.dest_def; moved abs_def to logic.ML; derived_def: conditional flag;

Toplevel.local_theory;

LocalDefs.cert_def; tuned;

eq_prop: Envir.beta_eta_contract;

renamed xxx_multi to xxx_list; tuned;

moved combound, rlist_abs to logic.ML;

union_tpairs: Library.merge; Envir.(beta_)eta_contract; tuned;

moved no_vars to sign.ML; removed dest_def (cf. Sign.cert_def);

lambda: abstract over any const; tuned;

added add_abbrevs(_i); moved const_of_class/class_of_const to logic.ML; added no_vars (from theory.ML); added cert_def; added const_expansion; certify: refer to Consts.certify, which includes expansion;

moved (beta_)eta_contract to envir.ML; tuned;

tuned;

added generic dest_def (mostly from theory.ML); added abs_def (from Isar/local_defs.ML); added const_of_class/class_of_const (from sign.ML); added combound, rlist_abs (from unify.ML);

added (beta_)eta_contract (from pattern.ML); added expand_atom;

print_theory: const abbreviations;

added abbreviations; added certify (mostly from sign.ML);

load envir.ML and logic.ML early;

Logic.rlist_abs;

Logic.const_of_class/class_of_const;

TableFun: renamed xxx_multi to xxx_list;

replaced Symtab.merge_multi by local merge_rules;

Envir.(beta_)eta_contract;

subsituted gen_duplicates / has_duplicates for duplicates whenever appropriate

added strip_abs

clarified semantics of merge

speedup: use simproc for AC rules

UU_reorient_simproc no longer rewrites UU = numeral

removed obsolete gen_ins/mem; added merge -- supercedes gen_merge_lists';

removed add/del_rules;

canonical member/insert/merge;

removal of case analysis clauses

fix

minor improvements

refined signature of locale module

no toplevel 'thy' anymore

fix in codegen

do not open structure;

reimplemented using Equiv_Relations.thy

improvement in devarifications

alternative syntax for instances

tuned;

consumes: negative argument relative to total number of prems;

added refine_insert;

Proof.refine_insert; statements: always use Attrib.src;

always use Attrib.src;

more generic type for map_specs/facts;

'obtains' element;

'obtain': optional case name;

index elements;

* Isar: 'obtains' element;

tuned msg;

theorem(_in_locale): Element.statement, Obtain.statement;

added parname; added (general_)statement (from isar_syn.ML); general_statement: Elements.statement, i.e. Shows/Obtains;

obtain(_i): optional name for 'that'; added statement (cf. Locale.theorem);

tuned comments;

moved (general_)statement to outer_parse.ML;

added concluding statements: Shows/Obtains;

moved specific map_typ/term to sign.ML;

added specific map_typ/term (from term.ML);

Exporting recdef's hints for use by new recdef package

*_asms_of fixed.

add 64bit atbroy98 platform

updated;

Added "evaluation" method and oracle.

new and updated protocol proofs by Giamp Bella

substantial cleanup and simplifications

name clarifications

added map_entry_yield

- renamed some lemmas (some had names coming from ancient versions of the nominal work) - some tuning - eventually this theory should be renamed to CR

added all constructors from PhD

axiomatization: retrict parameters to occurrences in specs; definition: restrict parameters to individual rhs;

improved comments;

tuned LocalDefs.unfold;

(un)fold: removed '(raw)' option;

added consts_retricted; pretty/print_consts: parameter restriction;

(un)fold: no raw flag; tuned;

tuned;

tuned LocalTheory.pretty_consts;

(un)folded: removed '(raw)' option;

lambda: abstract over TYPE argument, too;

tuned comments;

removal of ResClause.num_of_clauses and other simplifications

working SPASS support; much tidying

added serialization for arbitrary

minor change to CodegenPackage interface

minor cleanups

more coherent lookup extraction functions

reorganization of code to support DFG otuput

* Pure: 'advanced' translation functions use Context.generic instead of just theory;

declare defn rules;

all styles now reset to defaults first, i.e. the document may switch styles back and forth; added macro \isachardefaults for \chardef defaults; renamed \isakeywordcharunderscore to \isacharunderscorekeyword; added isabellestyle{default};

export meta_rewrite_rule; tuned;

advanced translations: Context.generic; tuned;

advanced translations: Context.generic;

tidy-up of res_clause.ML, removing the "predicates" field

'setup': no list type, support implicit setup; tuned;

'fixes': support plain vars; classical attributes: optional weight -- ignored by automated tools;

fixed a syntax error!

replaced gen_list by enum

adaptions to codegen_package

various improvements

added three times overloaded Isar instance command

moved instance Isar command to class_package.ML

added map_atype, map_aterms

tuned proof;

declare atomize/defn for Ball;

invent_fixes: merely enter body temporarily;

'unfolding': LocalDefs.unfold;

moved treatment of object-logic equalities to local_defs.ML;

method (un)folded: option '(raw)';

added attributes defn_add/del; added (un)fold operations (from object_logic.ML); tuned;

added 'defn' attribute; attribute (un)folded: option '(raw)';

proper order of trfuns;

CPure: Context.add_setup;

tuned proofs;

implicit setup;

default rule step: norm_hhf_tac;

tuned comment;

declare 'defn' rules;

LocalDefs;

Basic operations on local definitions.

removed unnecessary Syntax.fix_mixfix;

added axiomatization_loc, definition_loc; definition: let LocalDefs.derived_def do the actual work;

moved local defs to local_defs.ML;

LocalDefs; unfolding(_i): support object-level rewrites;

removed unatomize; added versions of meta_rewrite, unfold, fold;

(un)fold: support object-level rewrites;

added print_consts; tuned;

removed obsolete keyword 'files';

(un)folded: support object-level rewrites;

added equals_cong;

added Isar/local_defs.ML;

LocalDefs.add_def;

LocalDefs.def_export;

tuned proofs;

Pure/Isar: (un)folded, (un)fold, unfolding support object-level rewrite rules; ML/Isar: installed ML toplevel pretty printer for type Proof.context;

interrupt_timeout for Poly replaced by stub

added atomize_iff;

renamed Pretty.gen_list to Pretty.enum;

swapped theory_context;

swapped Toplevel.theory_context; definition(_i): actually rulify as well, support more of object-logic; definition(_i): more precise treatment of local fixes;

added invent_fixes; added debug flag, pprint_context;

swapped Toplevel.theory_context; tuned;

renamed reverse_atomize to unatomize; added rulify_term/tac;

init: include view; swapped Toplevel.theory_context; removed obsolete smart_note_thmss; moved note_thmss_qualified to PureThy; unified code of note_thmss(_i), add_thmss, locale_results;

improved 'notes', including proper treatment of locale results; tuned;

swapped Toplevel.theory_context;

Locale.init;

renamed gen_list to enum; added separate; tuned;

moved theorem tags from Drule to PureThy; replaced kind attribute by kind string; tuned name_multi: index > 1 only; added note_thmss_qualified (from Isar/locale.ML);

added ProofContext.pprint_context (depends on ProofContext.debug);

moved theorem tags from Drule to PureThy;

tidying up SPASS output

tidying

better reporting

Interface to access the specification of a named locale.

Added new file Tools/ATP/reduce_axiomsN.ML

Added in new file Tools/ATP/reduce_axiomsN.ML

Changed codes that call relevance filter.

Relevance filtering. Has replaced the previous version.

interrupt_timeout now raises Interrupt instead of SML90.Interrupt

smaller example to prevent timeout