| Wed, 17 Mar 1999 16:33:00 +0100 |
wenzelm |
qualify Theory.sign_of etc.;
|
file |
diff |
annotate
|
| Wed, 03 Feb 1999 16:45:45 +0100 |
wenzelm |
added Goal(w) and Export (from context.ML);
|
file |
diff |
annotate
|
| Fri, 15 Jan 1999 16:13:31 +0100 |
oheimb |
removed empty line (in case of empty begin_state marker) before Level line
|
file |
diff |
annotate
|
| Fri, 04 Dec 1998 10:45:20 +0100 |
paulson |
better export for nested locales
|
file |
diff |
annotate
|
| Wed, 25 Nov 1998 13:57:17 +0100 |
wenzelm |
removed redirect_to_latex stuff;
|
file |
diff |
annotate
|
| Thu, 29 Oct 1998 14:32:43 +0100 |
wenzelm |
tuned current_goals_markers semantics to avoid empty lines;
|
file |
diff |
annotate
|
| Fri, 23 Oct 1998 18:48:25 +0200 |
paulson |
better reporting of "Additional hypotheses" in a locale
|
file |
diff |
annotate
|
| Thu, 22 Oct 1998 20:07:42 +0200 |
wenzelm |
support current_goals_markers ref variable for print_current_goals;
|
file |
diff |
annotate
|
| Mon, 05 Oct 1998 10:31:43 +0200 |
paulson |
Now prove_goalw_cterm never prints timing statistics
|
file |
diff |
annotate
|
| Thu, 13 Aug 1998 17:43:00 +0200 |
paulson |
Rule mk_triv_goal for making instances of triv_goal
|
file |
diff |
annotate
|
| Tue, 04 Aug 1998 18:22:04 +0200 |
wenzelm |
added export: thm -> thm;
|
file |
diff |
annotate
|
| Mon, 29 Jun 1998 21:33:35 +0200 |
wenzelm |
moved actual (C)Pure theories to pure.ML;
|
file |
diff |
annotate
|
| Wed, 17 Jun 1998 10:48:38 +0200 |
nipkow |
Goals may now contain assumptions, which are not returned.
|
file |
diff |
annotate
|
| Fri, 05 Jun 1998 14:23:27 +0200 |
wenzelm |
tuned print_exn;
|
file |
diff |
annotate
|
| Sat, 22 Nov 1997 13:27:02 +0100 |
wenzelm |
fixed warning;
|
file |
diff |
annotate
|
| Fri, 21 Nov 1997 15:27:43 +0100 |
wenzelm |
changed Sequence interface (now Seq, in seq.ML);
|
file |
diff |
annotate
|
| Wed, 12 Nov 1997 16:21:26 +0100 |
wenzelm |
moved 'latex' from library.ML to goals.ML;
|
file |
diff |
annotate
|
| Fri, 24 Oct 1997 17:14:02 +0200 |
wenzelm |
Pure.thy;
|
file |
diff |
annotate
|
| Thu, 23 Oct 1997 12:10:55 +0200 |
wenzelm |
Sign.stamp_names_of;
|
file |
diff |
annotate
|
| Mon, 13 Oct 1997 17:47:59 +0200 |
wenzelm |
uses Sign.str_of_sort;
|
file |
diff |
annotate
|
| Thu, 25 Sep 1997 12:10:07 +0200 |
paulson |
Prints warnings using the "warning" function instead of "writeln"
|
file |
diff |
annotate
|
| Thu, 11 Sep 1997 16:16:03 +0200 |
wenzelm |
removed print_goals_ref (which was broken anyway);
|
file |
diff |
annotate
|
| Fri, 18 Jul 1997 14:06:54 +0200 |
wenzelm |
tuned error propagation msg;
|
file |
diff |
annotate
|
| Fri, 18 Jul 1997 13:52:35 +0200 |
wenzelm |
tuned warnings;
|
file |
diff |
annotate
|
| Wed, 16 Apr 1997 18:22:10 +0200 |
wenzelm |
Sorts.str_of_sort;
|
file |
diff |
annotate
|
| Wed, 02 Apr 1997 17:28:27 +0200 |
wenzelm |
changed signature of dummy goal from proto_pure to pure;
|
file |
diff |
annotate
|
| Tue, 04 Feb 1997 10:33:58 +0100 |
paulson |
Gradual switching to Basis Library functions nth, drop, etc.
|
file |
diff |
annotate
|
| Fri, 17 Jan 1997 11:13:18 +0100 |
paulson |
Added the prlim command
|
file |
diff |
annotate
|
| Fri, 08 Nov 1996 14:07:56 +0100 |
paulson |
Removed "standard" call from uresult, to allow specialist applications
|
file |
diff |
annotate
|
| Thu, 24 Oct 1996 10:42:42 +0200 |
paulson |
Allowing negative levels (as offsets) in prlev and choplev
|
file |
diff |
annotate
|