| Sat, 08 Jul 2006 12:54:37 +0200 |
wenzelm |
Goal.prove: context;
|
file |
diff |
annotate
|
| Sat, 27 May 2006 17:41:59 +0200 |
wenzelm |
unfold/refold: LocalDefs.meta_rewrite_rule;
|
file |
diff |
annotate
|
| Sat, 21 Jan 2006 23:02:20 +0100 |
wenzelm |
simplified type attribute;
|
file |
diff |
annotate
|
| Thu, 19 Jan 2006 21:22:08 +0100 |
wenzelm |
setup: theory -> theory;
|
file |
diff |
annotate
|
| Tue, 25 Oct 2005 18:18:49 +0200 |
wenzelm |
avoid legacy goals;
|
file |
diff |
annotate
|
| Fri, 21 Oct 2005 18:14:34 +0200 |
wenzelm |
Goal.prove;
|
file |
diff |
annotate
|
| Fri, 16 Sep 2005 01:42:57 +0200 |
huffman |
use mem operator
|
file |
diff |
annotate
|
| Thu, 15 Sep 2005 23:46:22 +0200 |
huffman |
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
|
file |
diff |
annotate
|
| Mon, 12 Sep 2005 23:18:01 +0200 |
huffman |
add header
|
file |
diff |
annotate
|
| Mon, 12 Sep 2005 23:14:41 +0200 |
huffman |
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
|
file |
diff |
annotate
|
| Mon, 12 Sep 2005 23:06:24 +0200 |
huffman |
new implementation of transfer principle
|
file |
diff |
annotate
|