Sat, 28 Aug 2010 13:41:31 +0800 |
Christian Urban |
updated to new Isabelle
|
changeset |
files
|
Fri, 27 Aug 2010 23:26:00 +0800 |
Christian Urban |
cut out most of the lifting section and cleaned up everything
|
changeset |
files
|
Fri, 27 Aug 2010 19:06:30 +0800 |
Christian Urban |
made all typographic changes
|
changeset |
files
|
Fri, 27 Aug 2010 16:00:19 +0800 |
Christian Urban |
first pass on section 1
|
changeset |
files
|
Fri, 27 Aug 2010 13:57:00 +0800 |
Christian Urban |
make copies of the "old" files
|
changeset |
files
|
Fri, 27 Aug 2010 02:25:40 +0000 |
Cezary Kaliszyk |
Ball Bex can be lifted after unfolding.
|
changeset |
files
|
Fri, 27 Aug 2010 03:37:17 +0800 |
Christian Urban |
"isabelle make test" makes all major examples....they work up to supp theorems (excluding)
|
changeset |
files
|
Fri, 27 Aug 2010 02:08:36 +0800 |
Christian Urban |
merged
|
changeset |
files
|
Fri, 27 Aug 2010 02:03:52 +0800 |
Christian Urban |
corrected bug with fv-function generation (that was the problem with recursive binders)
|
changeset |
files
|
Thu, 26 Aug 2010 14:55:15 +0900 |
Cezary Kaliszyk |
minor
|
changeset |
files
|
Thu, 26 Aug 2010 02:08:00 +0800 |
Christian Urban |
cleaned up (almost completely) the examples
|
changeset |
files
|
Wed, 25 Aug 2010 23:16:42 +0800 |
Christian Urban |
cleaning of unused files and code
|
changeset |
files
|
Wed, 25 Aug 2010 22:55:42 +0800 |
Christian Urban |
automatic lifting
|
changeset |
files
|
Wed, 25 Aug 2010 20:19:10 +0800 |
Christian Urban |
everything now lifts as expected
|
changeset |
files
|
Wed, 25 Aug 2010 11:58:37 +0800 |
Christian Urban |
now every lemma lifts (even with type variables)
|
changeset |
files
|