tuned signature;

allow 'for' fixes for multi_specs;

support 'assumes' in specifications, e.g. 'definition', 'inductive';
tuned signatures;

prefer tactics with explicit context;

renamed ML funs

local setup of induction tools, with restricted access to auxiliary consts;
proper antiquotations for formerly inaccessible consts;

@{command_spec} is superseded by @{command_keyword};

tuned signature;

clarified case_tac fixes and context;

proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
occasionally clarified use of context;

support (finite values of) codatatypes in Quickcheck

speed up old Nominal by killing type variables

ported old Nominal to use new datatypes

use compatibility layer

renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place

--HG--
rename : src/HOL/Datatype.thy => src/HOL/Old_Datatype.thy
rename : src/HOL/Tools/Function/size.ML => src/HOL/Tools/Function/old_size.ML
rename : src/HOL/Tools/Datatype/datatype.ML => src/HOL/Tools/Old_Datatype/old_datatype.ML
rename : src/HOL/Tools/Datatype/datatype_aux.ML => src/HOL/Tools/Old_Datatype/old_datatype_aux.ML
rename : src/HOL/Tools/Datatype/datatype_codegen.ML => src/HOL/Tools/Old_Datatype/old_datatype_codegen.ML
rename : src/HOL/Tools/Datatype/datatype_data.ML => src/HOL/Tools/Old_Datatype/old_datatype_data.ML
rename : src/HOL/Tools/Datatype/datatype_prop.ML => src/HOL/Tools/Old_Datatype/old_datatype_prop.ML
rename : src/HOL/Tools/Datatype/datatype_realizer.ML => src/HOL/Tools/Old_Datatype/old_datatype_realizer.ML
rename : src/HOL/Tools/Datatype/primrec.ML => src/HOL/Tools/Old_Datatype/old_primrec.ML
rename : src/HOL/Tools/Datatype/rep_datatype.ML => src/HOL/Tools/Old_Datatype/old_rep_datatype.ML

tuned structure inclusion

more antiquotations;

proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
clarified tool context in some boundary cases;

simplifier uses proper Proof.context instead of historic type simpset;

more standard module name Axclass (according to file name);

formal proof context for axclass proofs;
avoid global_simpset_of -- refer to simpset of proof context;

outer syntax command definitions based on formal command_spec derived from theory header declarations;

Corrected pt_set_inst, added missing cp_set_inst, deleted obsolete
pt_insert_eqvt, pt_set_eqvt, and perm_set_eq

treatment of type constructor `set`

'datatype' specifications allow explicit sort constraints;
tuned signatures;

discontinued obsolete datatype "alt_names";

modernized structure Induct_Tacs;

tuned specifications

assert Pure equations for theorem references; tuned

Finally removed old primrec package, since Primrec.add_primrec_global
can be used instead.

eliminated dead code;

renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;

--HG--
rename : src/Pure/pure_thy.ML => src/Pure/global_theory.ML

"prod" and "sum" replace "*" and "+" respectively

tuned quotes, antiquotations and whitespace

prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
eliminated old-style structure aliases K = Keyword, P = Parse;

adapted Theory_Data;
tuned;

eliminated hard tabulators, guessing at each author's individual tab-width;
tuned headers;

replaced String.concat by implode;
replaced String.concatWith by space_implode;
replaced (Seq.flat o Seq.map) by Seq.maps;
replaced List.mapPartial by map_filter;
replaced List.concat by flat;
replaced (flat o map) by maps, which produces less garbage;

tuned interfaces of datatype module

add_datatypes does not yield particular rules any longer

add_datatype interface yields type names and less rules

simplified names of common datatype types

discontinued ancient tradition to suffix certain ML module names with "_package"

--HG--
rename : src/HOL/Import/import_package.ML => src/HOL/Import/import.ML
rename : src/HOL/Nominal/nominal_package.ML => src/HOL/Nominal/nominal.ML
rename : src/HOL/Tools/specification_package.ML => src/HOL/Tools/choice_specification.ML
rename : src/HOL/Tools/datatype_package/datatype_package.ML => src/HOL/Tools/datatype_package/datatype.ML
rename : src/HOL/Tools/function_package/fundef_package.ML => src/HOL/Tools/function_package/fundef.ML
rename : src/HOL/Tools/inductive_package.ML => src/HOL/Tools/inductive.ML
rename : src/HOL/Tools/inductive_set_package.ML => src/HOL/Tools/inductive_set.ML
rename : src/HOL/Tools/old_primrec_package.ML => src/HOL/Tools/old_primrec.ML
rename : src/HOL/Tools/primrec_package.ML => src/HOL/Tools/primrec.ML
rename : src/HOL/Tools/recdef_package.ML => src/HOL/Tools/recdef.ML
rename : src/HOL/Tools/record_package.ML => src/HOL/Tools/record.ML
rename : src/HOL/Tools/typecopy_package.ML => src/HOL/Tools/typecopy.ML
rename : src/HOL/Tools/typedef_package.ML => src/HOL/Tools/typedef.ML

datatype packages: record datatype_config for configuration flags; less verbose signatures

explicit type_name antiquotations

proper spacing before ML antiquotations -- note that @ may be part of symbolic ML identifiers;

more uniform handling of binding in packages;

Made Option a separate theory and renamed option_map to Option.map

Merge.

Added equivariance lemmas for fresh_star.

binding replaces bstring

changed the names of insert_eqvt and set_eqvt so that it is clear that they have preconditions

cleaned up binding module and related code

Some more functions for accessing information about atoms.

Added some more theorems to NominalData.

explicit type Name.binding for higher-specification elements;

added equivariance lemmas for ex1 and the

PureThy: dropped note_thmss_qualified, dropped _i suffix

added facts to lemma swap_simps and tuned lemma calc_atms

InductTacs.case_tac: removed obsolete declare, which is now part of Goal.prove;

InductTacs.case_tac with proper context and proper declaration of local variable;

polished interface of datatype package

adapted case_tac/induct_tac;

- Deleted arity proofs for set
- Produce specific instances of theorems insert_eqvt, set_eqvt and perm_set_eq

added more infrastructure for fresh_star

eliminated non-linear access to thy1 and thy12c;

removed redundant axiomatizations of XXX_infinite (fact already proven);

simplified get_thm(s): back to plain name argument;

auxiliary dynamic_thm(s) for fact lookup;

added eqvt-flag to subseteq-lemma

joined theories IntDef, Numeral, IntArith to theory Int

added new primrec package

map_product and fold_product

simplified interfaces for outer syntax;

proper Sign operations instead of Theory aliases;

changed the representation of atoms to datatypes over nats

Added equivariance lemmas for induct_forall.

modified proofs so that they are not using claset()

ClassPackage renamed to Class

re-eliminated Option.thy

split off theory Option for benefit of code generator

tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);

introduced symmetric variants of the lemmas for alpha-equivalence

constant op @ now named append

simplified DataFun interfaces;

add the lemma supp_eqvt and put the right attribute

fixes last commit

add two lemmas dealing with freshness on permutations.

simplified the proof of pt_set_eqvt (as suggested by Randy Pollack)

moved axclass module closer to core system

improved the equivariance lemmas for the quantifiers; had to export the lemma eqvt_force_add and eqvt_force_del in the thmdecls

deleted remaining instances of swap_simp_a and swap_simp_b (obsolete now)

tuned slightly the previous commit

perm_simp can now simplify using the rules (a,b) o a = b and (a,b) o b = a

added pt_bij' to the collection perm_swap and also added abs_perm to the collection of equivariance lemmas

made the type sets instance of the "cp" type-class

added extended the lemma for equivariance of freshness

major update of the nominal package; there is now an infrastructure
for equivariance lemmas which eases definitions of nominal functions

Adapted to changes in Finite_Set theory.

removed legacy ML bindings;

replaced exists_fresh lemma with a version formulated with obtains;
old lemma is available as exists_fresh' (still needed in apply-scripts)

deleted all uses of sign_of as it's now the identity function

Removed non-trivial definitions from calc_atm theorem list.

adaption to argument change in primrec_package

replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes

Goal.prove_global;

added simplification rules to the fresh_guess tactic

made calc_atm stronger by including some relative
obvious simplification rules

added more infrastructure for the recursion combinator

added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
(they are used in the proof of the strong
induction principle)

added code to nominal_atoms to collect these
lemmas in "fresh_aux" instantiated for each
atom type

deleted the fresh_fun_eqvt from nominal_atoms,
since fresh_fun is not used anymore in the recursion
combinator

unchecked definitions;

added the lemma abs_fun_eq' to the nominal theory,
and also added code to nominal_atoms for generating
the theorem-list alpha'

added lemma fresh_right, which is useful
in the proof of the recursion combinator

AxClass.define_class_i;

Renamed "nominal" theory to "Nominal".

Adapted to new interface of add_axclass_i.

isar-keywords.el
- I am not sure what has changed here

nominal.thy
- includes a number of new lemmas (including freshness
and perm_aux things)

nominal_atoms.ML
- no particular changes here

nominal_permeq.ML
- a new version of the decision procedure using
for permutation composition the constant perm_aux

examples
- various adjustments

add_inst_arity_i renamed to prove_arity.

added fresh_fun_eqvt theorem to the theorem collection

improved the decision-procedure for permutations;
now uses a simproc

FIXME:
the simproc still needs to be adapted for arbitrary
atom types

Reverted to old interface of AxClass.add_inst_arity(_i)

Adapted to Florian's recent changes to the AxClass package.

Updated to Isabelle 2006-01-23

made the change for setup-functions not returning functions
anymore

Use generic Simplifier.simp_add attribute instead
of Simplifier.simp_add_global.

rolled back the last addition since these lemmas were already
in the simpset.

added the thms-collection "pt_id" (collection of all pt_<ak>1 lemmas)

added some lemmas to the collection "abs_fresh"

the lemmas are of the form

finite (supp x) ==> (b # [a].x) = (b=a \/ b # x)

previously only lemmas of the form

(b # [a].x) = (b=a \/ b # x)

with the type-constraint that x is finitely supported
were included.

added private datatype nprod (copy of prod) to be
used in the induction rule

changed the name of the type "nOption" to "noption".

made the changes according to Florian's re-arranging of
tuples (everything up to 19th December).

added proofs to show that every atom-kind combination
is in the respective finite-support class (now have to
adjust the files according to Florian's changes)

added thms to perm_compose (so far only composition
theorems were included where the type of the permutation
was equal)

tuned one comment

more cleaning up - this time of the cp-instance
proofs

improved the finite-support proof

added finite support proof for options (I am
surprised that one does not need more fs-proofs;
at the moment only lists, products, units and
atoms are shown to be finitely supported (of
course also every nominal datatype is finitely
supported))

deleted pt_bool_inst - not necessary because discrete
types are treated separately in nominal_atoms

improved the code for showing that a type is
in the pt-axclass (I try to slowly overcome
my incompetence with such ML-code).

added container-lemma fresh_eqvt


(definition: container-lemma contains all instantiations
of a lemma from the general theory)

added a fresh_left lemma that contains all instantiation
for the various atom-types.

changed the types in accordance with Florian's changes

Adapted to new type of PureThy.add_defs_i.

added code to say that discrete types (nat, bool, char)
are instances of cp_*_*.

added facilities to prove the pt and fs instances
for discrete types

made some of the theorem look-ups static (by using
thm instead of PureThy.get_thm)

finished cleaning up the parts that collect
lemmas (with instantiations) under some
general names

used the function Library.product for the cprod from Stefan

Moved atom stuff to new file nominal_atoms.ML