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;