| Sat, 04 Nov 2000 18:39:44 +0100 |
wenzelm |
misc stuff;
|
changeset |
files
|
| Fri, 03 Nov 2000 21:35:59 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 03 Nov 2000 21:35:36 +0100 |
wenzelm |
proper setup of "parallel";
|
changeset |
files
|
| Fri, 03 Nov 2000 21:34:22 +0100 |
wenzelm |
tuned notation;
|
changeset |
files
|
| Fri, 03 Nov 2000 21:33:53 +0100 |
wenzelm |
adapted "obtain" proofs;
|
changeset |
files
|
| Fri, 03 Nov 2000 21:33:15 +0100 |
wenzelm |
provide case names for rev_induct, rev_cases;
|
changeset |
files
|
| Fri, 03 Nov 2000 21:32:41 +0100 |
wenzelm |
rev_exhaust: rulify;
|
changeset |
files
|
| Fri, 03 Nov 2000 21:31:53 +0100 |
wenzelm |
removed atomic_Trueprop (now in Pure/Isar/auto_bind.ML);
|
changeset |
files
|
| Fri, 03 Nov 2000 21:31:11 +0100 |
wenzelm |
"atomize" for classical tactics;
|
changeset |
files
|
| Fri, 03 Nov 2000 21:29:56 +0100 |
wenzelm |
atomize: all automated tactics that "solve" goals;
|
changeset |
files
|
| Fri, 03 Nov 2000 21:28:15 +0100 |
wenzelm |
fixed two obscurities of "fix": predeclare_terms;
|
changeset |
files
|
| Fri, 03 Nov 2000 21:27:36 +0100 |
wenzelm |
tuned names;
|
changeset |
files
|
| Fri, 03 Nov 2000 21:27:06 +0100 |
wenzelm |
improved handling of "that": insert into goal, only declare as Pure "intro";
|
changeset |
files
|
| Fri, 03 Nov 2000 21:26:11 +0100 |
wenzelm |
assumption / finish: handle non-atomic assumptions from context as well;
|
changeset |
files
|