| Fri, 20 Jun 2008 17:43:16 +0200 |
huffman |
tweak lemmas adm_all and adm_ball
|
changeset |
files
|
| Thu, 19 Jun 2008 22:50:58 +0200 |
huffman |
move lemmas into locales;
|
changeset |
files
|
| Thu, 19 Jun 2008 22:43:59 +0200 |
huffman |
add lemmas take_chain_less and take_chain_le
|
changeset |
files
|
| Thu, 19 Jun 2008 22:27:10 +0200 |
wenzelm |
disposed Sign.read_typ etc;
|
changeset |
files
|
| Thu, 19 Jun 2008 22:05:05 +0200 |
wenzelm |
renamed is_abbrev_mode to abbrev_mode;
|
changeset |
files
|
| Thu, 19 Jun 2008 22:05:04 +0200 |
wenzelm |
ProofContext.abbrev_mode;
|
changeset |
files
|
| Thu, 19 Jun 2008 22:05:01 +0200 |
wenzelm |
moved get_sort to Isar/proof_context.ML;
|
changeset |
files
|
| Thu, 19 Jun 2008 21:14:30 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Thu, 19 Jun 2008 20:48:06 +0200 |
wenzelm |
private add_used (from drule.ML);
|
changeset |
files
|
| Thu, 19 Jun 2008 20:48:05 +0200 |
wenzelm |
Variable.declare_typ;
|
changeset |
files
|
| Thu, 19 Jun 2008 20:48:04 +0200 |
wenzelm |
added declare_typ;
|
changeset |
files
|
| Thu, 19 Jun 2008 20:48:03 +0200 |
wenzelm |
moved add_used to Isar/rule_insts.ML;
|
changeset |
files
|
| Thu, 19 Jun 2008 20:48:02 +0200 |
wenzelm |
export read_typ/cert_typ -- version with regular context operations;
|
changeset |
files
|
| Thu, 19 Jun 2008 20:48:01 +0200 |
wenzelm |
export read_typ/cert_typ -- version with regular context operations;
|
changeset |
files
|