| Tue, 09 Dec 2008 16:26:47 -0800 |
huffman |
use lemma lists defined in Int.thy
|
changeset |
files
|
| Wed, 10 Dec 2008 14:45:15 +0100 |
ballarin |
Merged.
|
changeset |
files
|
| Wed, 10 Dec 2008 14:21:42 +0100 |
ballarin |
Satisfy a_axioms.
|
changeset |
files
|
| Wed, 10 Dec 2008 10:12:44 +0100 |
ballarin |
Merged.
|
changeset |
files
|
| Wed, 10 Dec 2008 10:11:18 +0100 |
ballarin |
Enable keyword 'structure' in for clause of locale expression.
|
changeset |
files
|
| Tue, 09 Dec 2008 22:00:39 +0100 |
ballarin |
Correct order of defines in specification.
|
changeset |
files
|
| Tue, 09 Dec 2008 21:27:00 +0100 |
ballarin |
Pass on defines in inheritance; reject illicit defines created by instantiation.
|
changeset |
files
|
| Tue, 09 Dec 2008 15:34:49 +0100 |
ballarin |
Order of implicit parameters in locale expression.
|
changeset |
files
|
| Tue, 09 Dec 2008 13:11:42 +0100 |
ballarin |
NewLocale.intro_locales_tac added to Class.default_intro_tac.
|
changeset |
files
|
| Tue, 09 Dec 2008 11:30:24 +0100 |
ballarin |
When adding locales, delay notes until local theory is built.
|
changeset |
files
|
| Wed, 10 Dec 2008 10:28:16 +0100 |
nipkow |
merged
|
changeset |
files
|
| Wed, 10 Dec 2008 10:23:47 +0100 |
nipkow |
moved ContNotDenum into Library
|
changeset |
files
|
| Tue, 09 Dec 2008 15:31:38 -0800 |
huffman |
move lemmas from Numeral_Type.thy to other theories
|
changeset |
files
|
| Tue, 09 Dec 2008 12:53:25 -0800 |
huffman |
instantiation option :: (enum) enum
|
changeset |
files
|