| Mon, 01 Mar 2010 13:42:31 +0100 |
haftmann |
merged
|
file |
diff |
annotate
|
| Mon, 01 Mar 2010 13:40:23 +0100 |
haftmann |
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
|
file |
diff |
annotate
|
| Wed, 24 Feb 2010 21:59:21 +0100 |
wenzelm |
proper type syntax (cf. 7425aece4ee3);
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 14:43:18 +0200 |
wenzelm |
eliminated hard tabulators, guessing at each author's individual tab-width;
|
file |
diff |
annotate
|
| Mon, 21 Sep 2009 15:02:23 +0200 |
Christian Urban |
tuned some proofs
|
file |
diff |
annotate
|
| Fri, 03 Jul 2009 16:51:08 +0200 |
haftmann |
nominal.ML is nominal_datatype.ML
|
file |
diff |
annotate
|
| Fri, 19 Jun 2009 17:23:21 +0200 |
haftmann |
discontinued ancient tradition to suffix certain ML module names with "_package"
|
file |
diff |
annotate
|
| Sun, 26 Apr 2009 23:16:24 +0200 |
Christian Urban |
reorganised the section about fresh_star and added lemma pt_fresh_star_pi
|
file |
diff |
annotate
|
| Sat, 25 Apr 2009 21:42:05 +0200 |
Christian Urban |
adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 11:05:29 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 10:45:52 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Thu, 26 Feb 2009 16:34:03 +0100 |
berghofe |
Added postprocessing rules for fresh_star.
|
file |
diff |
annotate
|
| Wed, 25 Feb 2009 19:34:00 +0100 |
berghofe |
Added lemmas for normalizing freshness results involving fresh_star.
|
file |
diff |
annotate
|
| Wed, 25 Feb 2009 11:02:25 +0100 |
berghofe |
Added equivariance lemmas for fresh_star.
|
file |
diff |
annotate
|
| Sat, 14 Feb 2009 08:45:16 +0100 |
nipkow |
more finiteness changes
|
file |
diff |
annotate
|
| Tue, 16 Dec 2008 20:32:41 +0000 |
Christian Urban |
changed the names of insert_eqvt and set_eqvt so that it is clear that they have preconditions
|
file |
diff |
annotate
|
| Thu, 04 Dec 2008 14:43:33 +0100 |
haftmann |
cleaned up binding module and related code
|
file |
diff |
annotate
|
| Tue, 21 Oct 2008 21:18:54 +0200 |
berghofe |
Added nominal_inductive2.ML
|
file |
diff |
annotate
|
| Fri, 26 Sep 2008 14:51:27 +0200 |
berghofe |
Added some more lemmas that are useful in proof of strong induction rule.
|
file |
diff |
annotate
|
| Mon, 22 Sep 2008 19:46:24 +0200 |
urbanc |
made the perm_simp tactic to understand options such as (no_asm)
|
file |
diff |
annotate
|
| Wed, 27 Aug 2008 04:47:30 +0200 |
urbanc |
added equivariance lemmas for ex1 and the
|
file |
diff |
annotate
|
| Sun, 27 Jul 2008 20:08:16 +0200 |
urbanc |
simplified a proof
|
file |
diff |
annotate
|
| Fri, 27 Jun 2008 00:37:30 +0200 |
urbanc |
added a lemma to at_swap_simps
|
file |
diff |
annotate
|
| Mon, 16 Jun 2008 17:54:39 +0200 |
wenzelm |
allE_Nil: only one copy, proven in regular theory source;
|
file |
diff |
annotate
|
| Thu, 08 May 2008 04:20:08 +0200 |
urbanc |
added at_set_avoiding lemmas
|
file |
diff |
annotate
|
| Wed, 07 May 2008 10:57:19 +0200 |
berghofe |
Adapted to encoding of sets as predicates
|
file |
diff |
annotate
|
| Fri, 02 May 2008 22:43:14 +0200 |
urbanc |
added more infrastructure for fresh_star
|
file |
diff |
annotate
|
| Fri, 02 May 2008 16:32:51 +0200 |
urbanc |
polished the proof for atm_prm_fresh and more lemmas for fresh_star
|
file |
diff |
annotate
|
| Thu, 03 Apr 2008 11:48:48 +0200 |
urbanc |
added generalised definitions for freshness of sets of atoms
|
file |
diff |
annotate
|
| Wed, 19 Mar 2008 22:50:42 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|