| Sun, 14 Nov 2010 11:46:39 +0000 |
Christian Urban |
moved rest of the lemmas from Nominal2_FSet to the TypeScheme example
|
file |
diff |
annotate
|
| Sat, 06 Nov 2010 06:18:41 +0000 |
Christian Urban |
added a test about subtyping; disabled two tests, because of problem with function package
|
file |
diff |
annotate
|
| Thu, 14 Oct 2010 04:14:22 +0100 |
Christian Urban |
major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
|
file |
diff |
annotate
|
| Tue, 28 Sep 2010 05:56:11 -0400 |
Christian Urban |
added Foo1 to explore a contrived example
|
file |
diff |
annotate
|
| Mon, 27 Sep 2010 12:19:17 -0400 |
Christian Urban |
added postprocessed fresh-lemmas for constructors
|
file |
diff |
annotate
|
| Sat, 25 Sep 2010 08:28:45 -0400 |
Christian Urban |
cleaned up two examples
|
file |
diff |
annotate
|
| Mon, 20 Sep 2010 21:52:45 +0800 |
Christian Urban |
introduced a general procedure for structural inductions; simplified reflexivity proof
|
file |
diff |
annotate
|
| Sat, 04 Sep 2010 06:23:31 +0800 |
Christian Urban |
moved a proof to Abs
|
file |
diff |
annotate
|
| Sun, 29 Aug 2010 13:36:03 +0800 |
Christian Urban |
renamed NewParser to Nominal2
|
file |
diff |
annotate
|
| Sun, 29 Aug 2010 01:45:07 +0800 |
Christian Urban |
added fs-instance proofs
|
file |
diff |
annotate
|
| Sun, 29 Aug 2010 01:17:36 +0800 |
Christian Urban |
added proofs for fsupp properties
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 02:08:00 +0800 |
Christian Urban |
cleaned up (almost completely) the examples
|
file |
diff |
annotate
|
| Wed, 25 Aug 2010 22:55:42 +0800 |
Christian Urban |
automatic lifting
|
file |
diff |
annotate
|
| Sat, 21 Aug 2010 16:20:10 +0800 |
Christian Urban |
changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default
|
file |
diff |
annotate
|
| Sun, 27 Jun 2010 21:41:21 +0100 |
Christian Urban |
fixed according to changes in quotient
|
file |
diff |
annotate
|
| Wed, 02 Jun 2010 11:37:51 +0200 |
Christian Urban |
fixed problem with bn_info
|
file |
diff |
annotate
|
| Tue, 25 May 2010 18:38:52 +0200 |
Cezary Kaliszyk |
Substitution Lemma for TypeSchemes.
|
file |
diff |
annotate
|
| Tue, 25 May 2010 17:29:05 +0200 |
Cezary Kaliszyk |
Simplified the proof
|
file |
diff |
annotate
|
| Tue, 25 May 2010 17:09:29 +0200 |
Cezary Kaliszyk |
A lemma about substitution in TypeSchemes.
|
file |
diff |
annotate
|
| Wed, 12 May 2010 16:59:53 +0100 |
Christian Urban |
fixed the examples for the new eqvt-procedure....temporarily disabled Manual/Term4.thy
|
file |
diff |
annotate
|
| Tue, 11 May 2010 18:20:25 +0200 |
Cezary Kaliszyk |
Include raw permutation definitions in eqvt
|
file |
diff |
annotate
|
| Tue, 11 May 2010 17:16:57 +0200 |
Cezary Kaliszyk |
Declare alpha_gen_eqvt as eqvt and change the proofs that used 'eqvts[symmetric]'
|
file |
diff |
annotate
|
| Sun, 09 May 2010 12:26:10 +0100 |
Christian Urban |
cleaned up a bit the examples; added equivariance to all examples
|
file |
diff |
annotate
|
| Tue, 04 May 2010 11:12:09 +0200 |
Cezary Kaliszyk |
Move TypeSchemes to NewParser
|
file |
diff |
annotate
|
| Thu, 22 Apr 2010 05:16:23 +0200 |
Christian Urban |
moved lemmas from FSet.thy to do with atom to Nominal2_Base, and to do with 'a::at set to Nominal2_Atoms; moved Nominal2_Eqvt.thy one up to be loaded before Nominal2_Atoms
|
file |
diff |
annotate
|
| Thu, 08 Apr 2010 13:04:49 +0200 |
Christian Urban |
tuned type-schemes example
|
file |
diff |
annotate
|