hex and binary numerals (contributed by Rafal Kolanski)

minor optimization wrt. certifying terms

tuned;

tuned;

updated;

tuned interface; case_ss: proper context;

tuned interface;

removed dead code;

Element.prove_witness: context; Goal.prove_global;

prove_witness: context;

tuned exception handling;

prove/prove_multi: context; prove_global: theory + standard; tuned;

simprocs: no theory argument -- use simpset context instead; misc cleanup;

distinct simproc/simpset: proper context;

presburger_ss: proper context;

presburger_ss: proper context; Goal.prove: context;

tuned;

avoid Force_tac, which uses a different context;

Goal.prove: context;

tactic/method simpset: maintain proper context;

Goal.prove_global; SkipProof.prove: context;

Goal.prove_global;

simprocs: no theory argument -- use simpset context instead; tuned interfaces;

simprocs: no theory argument -- use simpset context instead;

updated;

updated Goal.prove, Goal.prove_global;

added some bits on variables;

* Pure: structure Variable provides operations for proper treatment of fixed/schematic variables; * Pure: Goal.prove, Goal.prove_global; tuned;

"solver" reference added to make the SAT solver configurable

Some tidying. Fixed a problem where the DFG file did not declare some TFrees as 0-ary functions. Frees no longer have types attached.

Fixed erroneous check-in.

made evaluation_conv and normalization_conv visible.

Internal restructuring: identify no longer computes syntax.

Modified comment.

added support for MiniSat 1.14

removed obsolete locale view;

apply_text: support Method.Source_i;

added method_i and Source_i;

thm parsers: include Args.internal_fact;

add/del_simps: warning for inactive simpset (no context); tuned;

updated;

Local variables;

Isar.context ();

tuned;

added Isar.context;

some tidying; fixed the output of theorem names

def_export: Drule.generalize;

matchers: fall back on plain first_order_matchers, not pattern;

make sure $DISTPREFIX exists before calling makedist

removed the "tagging" feature

made the conversion of elimination rules more robust

Literals aren't sorted any more.

Literals aren't sorted any more. Output overloaded constants' type var instantiations.

fixed let-simproc ----------------------------------------------------------------------

Isar: 'print_facts' prints all local facts;

print_lthms: include unnamed facts from index; tuned;

added content;

added props selector;

print_facts: all facts;

add_abbrevs/polymorphic: Variable.exportT_terms avoids over-generalization;

instantiate_tfrees: Thm.generalize;

removed parrot comment;

Proof by guessing.

guess: proper context for polymorphic parameters; tuned;

polymorphic: always generalize wrt. used_types;

varifyT: no longer pervasive;

added generalize/instantiate_option;

added map_proof_terms_option; tuned generalize, instantiate;

added generalize; removed obsolete assume_ax, tvars_intr_list;

Thm.varifyT;

added ex/Guess.thy;

skip_proofs: do not skip proofs of schematic goals (warning);

added schematic_goal;

added 'unfolding';

added simplification rules to the fresh_guess tactic

made calc_atm stronger by including some relative obvious simplification rules

Locales no longer generate views. The following functions have changed signatures: Locale.init, Locale.add_thmss, Locale.read/cert_context_statement.

added 'definition', 'unfolding', 'done'; tuned;

tuned;

added 'value'; tuned;

- put declarations inside a structure (NominalPermeq) - dynamic_thm(s) now looks up theorems in theory associated with proof state (rather than in context associated with simpset) - finite_guess_tac now automatically adds some extra rules about supp to the simpset

- nominal_permeq.ML is now loaded before nominal_package.ML - methods and tactics in nominal_permeq.ML are now defined inside structure NominalPermeq, therefore the names in the method_setup section had to be changed

Implemented proofs of equivariance and finite support for graph of recursion combinator.

Method intro_locales replaced by intro_locales and unfold_locales.

updated

Typo.

Minor new lemmas.

replaced respects2 by congruent2 because of type problem

replaced translation by abbreviation

obtain_export: Thm.generalize; guess: fixed handling of mixfixes of vars; tuned;

project_algebra: norm_sort; tuned;

comments fixed, minor optimization wrt. certifying terms

fix to subst in order to allow subst when head of a term is a bound variable.

CNF tactic invocations moved into comments

comment added

added more infrastructure for the recursion combinator

normal_form to lemma test

normalization uses refl now

Removed some incorrect axioms.

fixed stale theory bug

slight refinements

refinement in instance command

small change in class_package

added the "th" field to datatype Clause

fixed the "factor" method

new function norm_term

new method "normalization"

use -f in cp to overwrite read-only files (e.g. .svn in document/)

world map now transparent

improvements in Classpackage

reduced code, better instance command

slight improvements in code generation

added lookup function for parameters

disjunctive wellfoundedness

class package refinements, slight code generation refinements

added class projection

slight improvement

replaced subgraph by project

fix/fixes: tuned type constraints;

minor tuning of definitions/proofs;

fixed translations for _MapUpd: CONST;

beautification

added webmaster

Introduction of Ramsey's theorem

Removed debugging code.

Improved handling of defines imported in duplicate.

new standard dir structure

world map updated