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

world map updated

Removed (term_of o cterm_of)-Hack, Added error message for unknown definition at "termination"-command

fixed bug resolving Haskell names

fixed error bug

renamed thy data

Added split_cong rule

hyps better than prems

fixed sml/nj value restriction problem

Restructured locales with predicates: import is now an interpretation. New method intro_locales.

Fixed another variable order bug...

switched to open locales for classes

switched to open locales for classes

refrain from reforming TFL -- back to previous revision;

added declare_thm, thm_context; added trade(T);

eliminated freeze/varify in favour of Variable.import/export/trade;

world map updated

world map updated

Fixed name clash. Function-goals are now fully quantified. Avoiding large meta-conjunctions when setting up the goal. Cleanup.

world map updated

matchers: try pattern_matchers only *after* general matching (The pattern version is not a faithful approximation because it falls back on first-order matching!);

ProofContext.exports: simultaneous facts;

moved internal/skolem to term.ML;

mutual_rule: proper context;

export: simultaneous facts, refer to Variable.export; Term.internal/skolem;

ProofContext.exports: simultaneous facts; Variable.exportT_terms;

Variable.importT_inst; Term.internal;