| Wed, 04 Apr 2012 06:19:38 +0100 |
Christian Urban |
updated to Isabelle version April 1
|
file |
diff |
annotate
|
| Tue, 03 Jan 2012 11:43:27 +0000 |
Christian Urban |
updated to explicit set type constructor (post Isabelle 3rd January)
|
file |
diff |
annotate
|
| Mon, 05 Dec 2011 17:05:56 +0000 |
Christian Urban |
tiny improvement by removing one unnecessary assumption
|
file |
diff |
annotate
|
| Mon, 05 Dec 2011 15:34:12 +0000 |
Christian Urban |
tuned
|
file |
diff |
annotate
|
| Tue, 20 Sep 2011 14:44:50 +0900 |
Cezary Kaliszyk |
minor
|
file |
diff |
annotate
|
| Thu, 08 Sep 2011 13:03:19 +0100 |
Christian Urban |
more on paper
|
file |
diff |
annotate
|
| Tue, 05 Jul 2011 04:18:45 +0200 |
Christian Urban |
exported various FCB-lemmas to a separate file
|
file |
diff |
annotate
|
| Mon, 27 Jun 2011 19:15:18 +0100 |
Christian Urban |
fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction.
|
file |
diff |
annotate
|
| Mon, 20 Jun 2011 20:08:16 +0900 |
Cezary Kaliszyk |
Abs_set_fcb
|
file |
diff |
annotate
|
| Mon, 20 Jun 2011 09:59:18 +0900 |
Cezary Kaliszyk |
Move lst_fcb to Nominal2_Abs
|
file |
diff |
annotate
|
| Fri, 10 Jun 2011 15:30:09 +0900 |
Cezary Kaliszyk |
Slightly modify fcb for list1 and put in common place.
|
file |
diff |
annotate
|
| Mon, 28 Feb 2011 15:21:10 +0000 |
Christian Urban |
split the library into a basics file; merged Nominal_Eqvt into Nominal_Base
|
file |
diff |
annotate
|
| Thu, 24 Feb 2011 16:26:11 +0000 |
Christian Urban |
added a lemma about fresh_star and Abs
|
file |
diff |
annotate
|
| Tue, 01 Feb 2011 08:48:14 +0900 |
Cezary Kaliszyk |
More properties that relate abs_res and abs_set. Also abs_res with less binders.
|
file |
diff |
annotate
|
| Sun, 30 Jan 2011 12:09:23 +0900 |
Cezary Kaliszyk |
alpha_res implies alpha_set :)
|
file |
diff |
annotate
|