| Sat, 19 Feb 2011 09:31:22 +0900 |
Cezary Kaliszyk |
typeschemes/subst
|
file |
diff |
annotate
|
| Thu, 17 Feb 2011 17:02:25 +0900 |
Cezary Kaliszyk |
further experiments with typeschemes subst
|
file |
diff |
annotate
|
| Mon, 07 Feb 2011 15:59:37 +0000 |
Christian Urban |
cleaned up the experiments so that the tests go through
|
file |
diff |
annotate
|
| Tue, 01 Feb 2011 08:57:50 +0900 |
Cezary Kaliszyk |
Experiments with substitution on set+
|
file |
diff |
annotate
|
| Sun, 30 Jan 2011 09:57:37 +0900 |
Cezary Kaliszyk |
Showing that the binders difference is fresh for the left side solves the goal for 'set'.
|
file |
diff |
annotate
|
| Sat, 29 Jan 2011 14:26:47 +0900 |
Cezary Kaliszyk |
Experiments with functions
|
file |
diff |
annotate
|
| Thu, 27 Jan 2011 20:19:13 +0100 |
Christian Urban |
some experiments
|
file |
diff |
annotate
|
| Tue, 25 Jan 2011 18:58:26 +0100 |
Christian Urban |
made eqvt-proof explicit in the function definitions
|
file |
diff |
annotate
|
| Tue, 18 Jan 2011 21:26:58 +0100 |
Christian Urban |
some tryes about substitution over type-schemes
|
file |
diff |
annotate
|
| Fri, 31 Dec 2010 15:37:04 +0000 |
Christian Urban |
changed res keyword to set+ for restrictions; comment by a referee
|
file |
diff |
annotate
|
| Tue, 28 Dec 2010 19:51:25 +0000 |
Christian Urban |
automated all strong induction lemmas
|
file |
diff |
annotate
|
| Wed, 22 Dec 2010 21:13:44 +0000 |
Christian Urban |
tuned examples
|
file |
diff |
annotate
|
| Wed, 22 Dec 2010 09:13:25 +0000 |
Christian Urban |
properly exported strong exhaust theorem; cleaned up some examples
|
file |
diff |
annotate
|
| Thu, 16 Dec 2010 08:42:48 +0000 |
Christian Urban |
simple cases for strong inducts done; infrastructure for the difficult ones is there
|
file |
diff |
annotate
|
| 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
|