| Tue, 03 Apr 2007 17:05:52 +0200 |
narboux |
remove the lemma swap_fun which was not needed
|
file |
diff |
annotate
|
| Mon, 02 Apr 2007 23:24:52 +0200 |
narboux |
rename bij and fresh into bijs and freshs and lookup for eqvts lemma using the ml value instead of the name
|
file |
diff |
annotate
|
| Wed, 28 Mar 2007 18:25:23 +0200 |
urbanc |
the name for the collection of equivariance lemmas is now eqvts (changed from eqvt) in order to avoid clashes with eqvt-lemmas generated in nominal_inductive
|
file |
diff |
annotate
|
| Tue, 06 Mar 2007 15:28:22 +0100 |
urbanc |
major update of the nominal package; there is now an infrastructure
|
file |
diff |
annotate
|
| Wed, 07 Feb 2007 17:51:38 +0100 |
berghofe |
Adapted to changes in Finite_Set theory.
|
file |
diff |
annotate
|
| Wed, 06 Dec 2006 01:12:36 +0100 |
wenzelm |
removed legacy ML bindings;
|
file |
diff |
annotate
|
| Wed, 29 Nov 2006 15:44:51 +0100 |
wenzelm |
simplified method setup;
|
file |
diff |
annotate
|
| Fri, 20 Oct 2006 17:07:26 +0200 |
haftmann |
slight cleanup
|
file |
diff |
annotate
|
| Wed, 04 Oct 2006 14:17:38 +0200 |
haftmann |
insert replacing ins ins_int ins_string
|
file |
diff |
annotate
|
| Tue, 29 Aug 2006 21:43:34 +0200 |
urbanc |
added a FIXME-comment
|
file |
diff |
annotate
|
| Wed, 02 Aug 2006 22:26:41 +0200 |
wenzelm |
normalized Proof.context/method type aliases;
|
file |
diff |
annotate
|
| Tue, 04 Jul 2006 17:26:02 +0200 |
urbanc |
added simplification rules to the fresh_guess tactic
|
file |
diff |
annotate
|
| Tue, 04 Jul 2006 15:26:56 +0200 |
berghofe |
- put declarations inside a structure (NominalPermeq)
|
file |
diff |
annotate
|
| Mon, 12 Jun 2006 20:32:33 +0200 |
urbanc |
added lemma fresh_unit to Nominal.thy
|
file |
diff |
annotate
|
| Mon, 12 Jun 2006 18:17:21 +0200 |
berghofe |
Added fresh_guess_tac.
|
file |
diff |
annotate
|
| Fri, 28 Apr 2006 15:54:34 +0200 |
berghofe |
Renamed "nominal" theory to "Nominal".
|
file |
diff |
annotate
|
| Thu, 27 Apr 2006 01:41:30 +0200 |
urbanc |
isar-keywords.el
|
file |
diff |
annotate
|
| Thu, 06 Apr 2006 17:29:40 +0200 |
urbanc |
modified the perm_compose rule such that it
|
file |
diff |
annotate
|
| Wed, 01 Mar 2006 18:26:20 +0100 |
urbanc |
fixed a problem where a permutation is not analysed
|
file |
diff |
annotate
|
| Wed, 01 Mar 2006 10:27:01 +0100 |
urbanc |
made some small tunings in the decision-procedure
|
file |
diff |
annotate
|
| Mon, 27 Feb 2006 17:37:37 +0100 |
urbanc |
added a finite_guess tactic, which solves
|
file |
diff |
annotate
|
| Mon, 27 Feb 2006 12:14:36 +0100 |
urbanc |
added support for arbitrary atoms in the simproc
|
file |
diff |
annotate
|
| Sun, 26 Feb 2006 22:24:05 +0100 |
urbanc |
improved the decision-procedure for permutations;
|
file |
diff |
annotate
|
| Mon, 19 Dec 2005 12:08:16 +0100 |
urbanc |
fixed a bug that occured when more than one atom-type
|
file |
diff |
annotate
|
| Tue, 29 Nov 2005 01:37:01 +0100 |
urbanc |
made some of the theorem look-ups static (by using
|
file |
diff |
annotate
|
| Tue, 01 Nov 2005 23:54:29 +0100 |
urbanc |
tunings of some comments (nothing serious)
|
file |
diff |
annotate
|
| Sat, 29 Oct 2005 15:01:25 +0200 |
urbanc |
Changed Simplifier.simp_modifiers to Simplifier.simp_modifiers'.
|
file |
diff |
annotate
|
| Fri, 28 Oct 2005 16:43:46 +0200 |
urbanc |
Added (optional) arguments to the tactics
|
file |
diff |
annotate
|
| Mon, 17 Oct 2005 12:30:57 +0200 |
berghofe |
Initial revision.
|
file |
diff |
annotate
|