added generalize rule; added maxidx_thm;

added exists_subtype; added internal/skolem (from Syntax/lexicon.ML); added generalize(T);

added generalize rule;

Term.skolem;

Term.internal;

ProofContext.export: singleton;

RuleCases.mutual_rule: ctxt; ProofContext.exports: simultaneous facts;

RuleCases.mutual_rule: ctxt; Term.internal; ProofContext.exports: simultaneous facts;

added interface for making term contexts.

fixed symlink bug

ProofContext: moved variable operations to struct Variable; tuned;

Fixed type/term variables and polymorphic term abbreviations.

added variable.ML;

ProofContext: moved variable operations to struct Variable;

*** empty log message ***

*** empty log message ***

the "all_theorems" option and some fixes

the enumerate operator

Jia Meng added to world map

keyword update

slight adaption for code generator

slight adaptions for code generator

slight adaptions

slight refinements for code generator

added hook for case const defs

added codegen_simtype

improvements in code generator

avoid global Drule.unvarify;

tuned interfaces; added invent_types; added import_types/terms;

added hyps_of; tuned;

added equiv;

(un)varify: tuned exceptions;

removed weak_eq_thm; added equiv_thm; removed obsolete unvarifyT; improved unvarify -- demands global context (cf. Logic.unvarify);

Drule.equiv_thm supercedes Drule.weak_eq_thm;

tuned;

avoid unqualified exception names; tuned;

ProjectRule now context dependent;

use Drule.unvarify instead of obsolete Drule.freeze_all;

corrected w.r.t. search order for subst.

Corrected search order for zippers.

new results

removal of the obsolete "infinite_nonempty"

tuned;

added declare_typ; simult_matches: Unify.matchers;

tuned;

tuned interfaces;

added matchers, matches_list; tuned interfaces;

removed matches_seq -- didn't quite work;

Unify.matches_list;

tuned Seq/Envir/Unify interfaces;

fixed subst step;

avoid accidental binding of ?Jmp;

added lemma fresh_unit to Nominal.thy made the fresh_guess tactic to solve more goals adapted Iteration.thy to use the new tactic

Added fresh_guess_tac.

Removed comments around declaration of fresh_guess method.

Added "evaluation" method.

updated keywords

made smlnj happy;

fixed smlnj incompat.

Completely rewrote code for defining graph of recursion combinator.

fixed subst step;

actually invoke result elements;

improved treatment of TERM TYPE syntax;

added import -- fixes schematic variables; added export;

fixes: include mixfix syntax; goal: improved handling of implicit vars;

added for_fixes;

fixes: include mixfix syntax;

added satisfy_ctxt;

outer_params: Syntax.dest_internal;

avoid unqualified exception;

added quoting via back quotes

updated IsaMakefiles for new location of IsaPlanner.

removed IsaPlanner - these are now in Provers.

removed IsaPlannner things from Pure. Moved to Provers.

moved to new location in Provers.

added updated version of IsaPlanner and substitution.

unique_names no longer set to false (thanks to improved naming scheme for "internal" constructors).

- Changed naming scheme: names of "internal" constructors now have "_Rep" as suffix - no need to set unique_names to false any longer - Cleaned up a bit (removed occurrences of strip_option and replace_types')

nbe -> NormalForm

CVS: ----------------------------------------------------------------------

renamed command

renamed file

Removed "code del" declarations again.

fixed owner bug

less_equal -> less_eq (someone had screwd up here)

Splitting order changed.

added John's example

replaced REPEAT by REPOEAT_DETERM

gmake vs. make

removed obsolete ML files;

removed obsolete ML files;

removed obsolete ML files;

adding case theorems for code generator

slight code generator cleanup

removed 'primitive definitions' added (non)strict generation, minor fixes

fixed typo

* Theory syntax: some popular names (e.g. "class", "if") are now keywords. * Isar: schematic goals are no longer restricted to higher-order patterns. * ML/Pure: Logic.(un)varify only works in a global context, which is now enforced.

Schematic invocation of locale expression in proof context.

added invoke.ML;

added locale_insts;

renamed Type.(un)varifyT to Logic.(un)varifyT; made (un)varify strict wrt. global context -- may use legacy_(un)varify as workaround; renaming: removed duplicate, use zip_options;

added 'if' and 'for' keywords; tuned;

added facts_of; tuned interfaces;

added Tools/invoke.ML;

renamed Type.(un)varifyT to Logic.(un)varifyT; made (un)varify strict wrt. global context -- may use legacy_(un)varify as workaround;

do not open Logic;

tuned;

removed obsolete ML files;

removed obsolete ML files;

removed obsolete ML files;

removed Toplevel.debug;

added zip_options;

tuned;

updated;

quoted "if";

added type inference at the end of normalization

revised nbe command and examples

new lemmas concerning finite cardinalities

quoted "if";

refined code generation