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 