| Mon, 15 Mar 2010 22:22:28 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 15 Mar 2010 17:34:03 +0100 |
nipkow |
merged
|
changeset |
files
|
| Mon, 15 Mar 2010 17:33:41 +0100 |
nipkow |
tuned inductions
|
changeset |
files
|
| Mon, 15 Mar 2010 21:59:28 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 15 Mar 2010 21:57:35 +0100 |
wenzelm |
moved old Sign.intern_term to the place where it is still used;
|
changeset |
files
|
| Mon, 15 Mar 2010 20:27:23 +0100 |
wenzelm |
preserve full const name more carefully, and avoid slightly odd Sign.intern_term;
|
changeset |
files
|
| Mon, 15 Mar 2010 18:59:16 +0100 |
wenzelm |
replaced type_syntax/term_syntax by uniform syntax_declaration;
|
changeset |
files
|
| Mon, 15 Mar 2010 15:13:22 +0100 |
haftmann |
merged
|
changeset |
files
|
| Mon, 15 Mar 2010 15:13:07 +0100 |
haftmann |
corrected disastrous syntax declarations
|
changeset |
files
|
| Mon, 15 Mar 2010 13:59:34 +0100 |
haftmann |
added stmaryrd for isasymSqinter
|
changeset |
files
|
| Sun, 14 Mar 2010 19:48:33 -0700 |
huffman |
use headers consistently
|
changeset |
files
|
| Sun, 14 Mar 2010 19:47:13 -0700 |
huffman |
no_document for theory Countable
|
changeset |
files
|
| Sun, 14 Mar 2010 14:10:36 -0700 |
huffman |
old domain package also defines map functions
|
changeset |
files
|
| Sun, 14 Mar 2010 14:10:05 -0700 |
huffman |
separate map-related code into new function define_map_functions
|
changeset |
files
|
| Sun, 14 Mar 2010 15:50:17 +0100 |
Christian Urban |
removed Local_Theory.theory_result by using local Typedef.add_typedef
|
changeset |
files
|