20080507 
berghofe 
20080507 
Adapted to encoding of sets as predicates

file  diff  annotate 
20080320 
wenzelm 
20080320 
simplified get_thm(s): back to plain name argument;

file  diff  annotate 
20080319 
wenzelm 
20080319 
auxiliary dynamic_thm(s) for fact lookup;
renamed local dynamic_thm(s) to goal_thm(s);

file  diff  annotate 
20080128 
berghofe 
20080128 
Cleaned up simproc code.

file  diff  annotate 
20070913 
urbanc 
20070913 
some cleaning up to do with contexts

file  diff  annotate 
20070902 
urbanc 
20070902 
made theoremreferences safe

file  diff  annotate 
20070426 
wenzelm 
20070426 
eliminated unnamed infixes, tuned syntax;

file  diff  annotate 
20070413 
narboux 
20070413 
debug versions of finite_guess and fresh_guess do not fail if they can not solve the goal

file  diff  annotate 
20070407 
urbanc 
20070407 
tuned slightly the previous commit

file  diff  annotate 
20070407 
narboux 
20070407 
perm_simp can now simplify using the rules (a,b) o a = b and (a,b) o b = a

file  diff  annotate 
20070404 
narboux 
20070404 
make fresh_guess fail if it does not solve the subgoal

file  diff  annotate 
20070404 
wenzelm 
20070404 
removed obsolete sign_of/sign_of_thm;

file  diff  annotate 
20070403 
narboux 
20070403 
remove the lemma swap_fun which was not needed

file  diff  annotate 
20070402 
narboux 
20070402 
rename bij and fresh into bijs and freshs and lookup for eqvts lemma using the ml value instead of the name

file  diff  annotate 
20070328 
urbanc 
20070328 
the name for the collection of equivariance lemmas is now eqvts (changed from eqvt) in order to avoid clashes with eqvtlemmas generated in nominal_inductive

file  diff  annotate 
20070306 
urbanc 
20070306 
major update of the nominal package; there is now an infrastructure
for equivariance lemmas which eases definitions of nominal functions

file  diff  annotate 
20070207 
berghofe 
20070207 
Adapted to changes in Finite_Set theory.

file  diff  annotate 
20061206 
wenzelm 
20061206 
removed legacy ML bindings;

file  diff  annotate 
20061129 
wenzelm 
20061129 
simplified method setup;

file  diff  annotate 
20061020 
haftmann 
20061020 
slight cleanup

file  diff  annotate 
20061004 
haftmann 
20061004 
insert replacing ins ins_int ins_string

file  diff  annotate 
20060829 
urbanc 
20060829 
added a FIXMEcomment

file  diff  annotate 
20060802 
wenzelm 
20060802 
normalized Proof.context/method type aliases;

file  diff  annotate 
20060704 
urbanc 
20060704 
added simplification rules to the fresh_guess tactic

file  diff  annotate 
20060704 
berghofe 
20060704 
 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

file  diff  annotate 
20060612 
urbanc 
20060612 
added lemma fresh_unit to Nominal.thy
made the fresh_guess tactic to solve more goals
adapted Iteration.thy to use the new tactic

file  diff  annotate 
20060612 
berghofe 
20060612 
Added fresh_guess_tac.

file  diff  annotate 
20060428 
berghofe 
20060428 
Renamed "nominal" theory to "Nominal".

file  diff  annotate 
20060427 
urbanc 
20060427 
isarkeywords.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

file  diff  annotate 
20060406 
urbanc 
20060406 
modified the perm_compose rule such that it
is applied as simplification rule (as simproc)
in the restricted case where the first
permutation is a swapping coming from a supports
problem
also deleted the perm_compose' rule from the set
of rules that are automatically tried

file  diff  annotate 
20060301 
urbanc 
20060301 
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

file  diff  annotate 
20060301 
urbanc 
20060301 
made some small tunings in the decisionprocedure
(in the order how the "small" tactics are called)

file  diff  annotate 
20060227 
urbanc 
20060227 
added a finite_guess tactic, which solves
automatically finitesupport goals

file  diff  annotate 
20060227 
urbanc 
20060227 
added support for arbitrary atoms in the simproc

file  diff  annotate 
20060226 
urbanc 
20060226 
improved the decisionprocedure for permutations;
now uses a simproc
FIXME:
the simproc still needs to be adapted for arbitrary
atom types

file  diff  annotate 
20051219 
urbanc 
20051219 
fixed a bug that occured when more than one atomtype
is declared.

file  diff  annotate 
20051129 
urbanc 
20051129 
made some of the theorem lookups static (by using
thm instead of PureThy.get_thm)

file  diff  annotate 
20051101 
urbanc 
20051101 
tunings of some comments (nothing serious)

file  diff  annotate 
20051029 
urbanc 
20051029 
Changed Simplifier.simp_modifiers to Simplifier.simp_modifiers'.
This means the syntax of the tactics supports_simp and perm_simp
are exactly like simp, namely
(supports_simp add: .... del: ...)
where the add's and del's are optional.

file  diff  annotate 
20051028 
urbanc 
20051028 
Added (optional) arguments to the tactics
perm_eq_simp and supports_simp. They now
follow the "simp"way and use the syntax:
apply(supports_simp simp add: thms)
etc.

file  diff  annotate 
20051017 
berghofe 
20051017 
Initial revision.

file  diff  annotate 