| Fri, 13 Oct 2006 12:32:44 +0200 |
haftmann |
lifted claset setup from ML to Isar level
|
changeset |
files
|
| Fri, 13 Oct 2006 09:02:21 +0200 |
haftmann |
explicit nonfix for union and inter
|
changeset |
files
|
| Thu, 12 Oct 2006 22:57:45 +0200 |
wenzelm |
renamed enter_forward_proof to enter_proof_body;
|
changeset |
files
|
| Thu, 12 Oct 2006 22:57:42 +0200 |
wenzelm |
added peek;
|
changeset |
files
|
| Thu, 12 Oct 2006 22:57:38 +0200 |
wenzelm |
interpretation_in_locale: standalone goal setup;
|
changeset |
files
|
| Thu, 12 Oct 2006 22:57:35 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 12 Oct 2006 22:57:32 +0200 |
wenzelm |
renamed print_lthms to print_facts, do not insist on proof state;
|
changeset |
files
|
| Thu, 12 Oct 2006 22:57:29 +0200 |
wenzelm |
print_evaluated_term: Toplevel.context_of;
|
changeset |
files
|
| Thu, 12 Oct 2006 22:57:24 +0200 |
wenzelm |
replaced attributes_update by map_attributes;
|
changeset |
files
|
| Thu, 12 Oct 2006 22:57:20 +0200 |
wenzelm |
Toplevel.local_theory_to_proof: proper target;
|
changeset |
files
|
| Thu, 12 Oct 2006 22:57:15 +0200 |
wenzelm |
Toplevel.local_theory: proper target;
|
changeset |
files
|
| Thu, 12 Oct 2006 22:03:33 +0200 |
urbanc |
To be consistent with "induct", I renamed "fixing" to "arbitrary".
|
changeset |
files
|
| Thu, 12 Oct 2006 15:50:43 +0200 |
paulson |
Extended combinators now disabled
|
changeset |
files
|
| Thu, 12 Oct 2006 15:50:16 +0200 |
paulson |
abstraction is now turned OFF...
|
changeset |
files
|