| Sat, 18 Sep 2010 05:13:42 +0800 |
Christian Urban |
updated to Isabelle Sept 13
|
file |
diff |
annotate
|
| Sun, 12 Sep 2010 22:46:40 +0800 |
Christian Urban |
tuned code
|
file |
diff |
annotate
|
| Thu, 27 May 2010 18:30:26 +0200 |
Christian Urban |
fixed bug where perm_simp 'forgets' how to prove equivariance for the empty set
|
file |
diff |
annotate
|
| Thu, 13 May 2010 15:12:05 +0100 |
Christian Urban |
removed internal functions from the signature (they are not needed anymore)
|
file |
diff |
annotate
|
| Mon, 26 Apr 2010 13:08:14 +0200 |
Christian Urban |
rewrote eqvts_raw to be a symtab, that can be looked up
|
file |
diff |
annotate
|
| Sun, 25 Apr 2010 09:13:16 +0200 |
Christian Urban |
tuned and cleaned
|
file |
diff |
annotate
|
| Sun, 18 Apr 2010 17:57:27 +0200 |
Christian Urban |
tuned; transformation functions now take a context, a thm and return a thm
|
file |
diff |
annotate
|
| Wed, 14 Apr 2010 22:41:22 +0200 |
Christian Urban |
temporary fix for CoreHaskell
|
file |
diff |
annotate
|
| Wed, 14 Apr 2010 18:46:59 +0200 |
Christian Urban |
thmdecls can deal with lemmas like alpha_gen which contain pairs or tuples
|
file |
diff |
annotate
|
| Wed, 14 Apr 2010 16:05:58 +0200 |
Christian Urban |
tuned and removed dead code
|
file |
diff |
annotate
|
| Wed, 14 Apr 2010 15:02:07 +0200 |
Christian Urban |
moved a couple of more functions to the library
|
file |
diff |
annotate
|
| Mon, 12 Apr 2010 13:34:54 +0200 |
Christian Urban |
implemented in thmdecls the case where eqvt-lemmas are of the form _ ==> _
|
file |
diff |
annotate
|
| Sun, 11 Apr 2010 22:48:49 +0200 |
Christian Urban |
fixed bug in thmdecls with destructing Trueprop; some initial infrastructure for eqvt-theorems of the form _ ==> _
|
file |
diff |
annotate
|
| Fri, 09 Apr 2010 21:51:01 +0200 |
Christian Urban |
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
|
file |
diff |
annotate
|
| Sun, 04 Apr 2010 21:39:28 +0200 |
Christian Urban |
separated general nominal theory into separate folder
|
file |
diff |
annotate
| base
|