| Mon, 14 Jul 2008 17:51:43 +0200 |
wenzelm |
eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
|
changeset |
files
|
| Mon, 14 Jul 2008 17:51:42 +0200 |
wenzelm |
adapted IsarCmd.init_theory;
|
changeset |
files
|
| Mon, 14 Jul 2008 17:51:41 +0200 |
wenzelm |
renamed theory to init_theory, removed obsolete kill argument;
|
changeset |
files
|
| Mon, 14 Jul 2008 17:51:39 +0200 |
wenzelm |
added commit_exit;
|
changeset |
files
|
| Mon, 14 Jul 2008 17:47:18 +0200 |
krauss |
single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
|
changeset |
files
|
| Mon, 14 Jul 2008 17:02:55 +0200 |
krauss |
renamed conversions to _conv, tuned
|
changeset |
files
|
| Mon, 14 Jul 2008 16:13:58 +0200 |
chaieb |
Simplified proofs
|
changeset |
files
|
| Mon, 14 Jul 2008 16:13:55 +0200 |
chaieb |
Simple theorems about zgcd moved to GCD.thy
|
changeset |
files
|
| Mon, 14 Jul 2008 16:13:51 +0200 |
chaieb |
Theorem names as in IntPrimes.thy, also several theorems moved from there
|
changeset |
files
|
| Mon, 14 Jul 2008 16:13:42 +0200 |
chaieb |
Fixed proofs.
|
changeset |
files
|
| Mon, 14 Jul 2008 11:19:43 +0200 |
wenzelm |
ProofNode.current
|
changeset |
files
|
| Mon, 14 Jul 2008 11:19:42 +0200 |
wenzelm |
command 'redo' no longer available;
|
changeset |
files
|
| Mon, 14 Jul 2008 11:19:41 +0200 |
wenzelm |
replaced obsolete ProofHistory by ProofNode (backtracking only);
|
changeset |
files
|
| Mon, 14 Jul 2008 11:19:40 +0200 |
wenzelm |
removed obsolete 'redo' command;
|
changeset |
files
|