| Mon, 03 Feb 2003 11:07:09 +0100 |
berghofe |
Moved print_intros from proof_general.ML to Isar/isar_cmd.ML
|
file |
diff |
annotate
|
| Wed, 27 Nov 2002 17:16:47 +0100 |
berghofe |
Added some functions for processing PGIP (thanks to David Aspinall).
|
file |
diff |
annotate
|
| Mon, 14 Oct 2002 10:44:32 +0200 |
nipkow |
Ported find_intro/elim to Isar.
|
file |
diff |
annotate
|
| Wed, 28 Aug 2002 15:27:43 +0200 |
wenzelm |
improved tell_thm_deps;
|
file |
diff |
annotate
|
| Tue, 27 Aug 2002 15:40:58 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 27 Aug 2002 11:04:27 +0200 |
wenzelm |
result dependency output;
|
file |
diff |
annotate
|
| Thu, 18 Jul 2002 12:09:08 +0200 |
wenzelm |
fixed inform_file_retracted: remove_thy;
|
file |
diff |
annotate
|
| Tue, 02 Jul 2002 17:44:13 +0200 |
wenzelm |
thms_containing: optional limit argument;
|
file |
diff |
annotate
|
| Tue, 02 Jul 2002 15:38:13 +0200 |
wenzelm |
ProofContext.print_thms_containing;
|
file |
diff |
annotate
|
| Mon, 21 Jan 2002 22:27:34 +0100 |
wenzelm |
full_proofs;
|
file |
diff |
annotate
|
| Wed, 16 Jan 2002 21:01:08 +0100 |
wenzelm |
tuned title;
|
file |
diff |
annotate
|
| Wed, 16 Jan 2002 20:57:02 +0100 |
wenzelm |
Interface/proof_general.ML move to proof_general.ML;
|
file |
diff |
annotate
|