| Mon, 12 Jul 2010 21:38:37 +0200 |
wenzelm |
moved misc legacy stuff from OldGoals to Misc_Legacy;
|
file |
diff |
annotate
|
| Fri, 04 Jun 2010 16:53:08 +0200 |
blanchet |
"print_vars_terms" wasn't doing its job properly;
|
file |
diff |
annotate
|
| Thu, 27 May 2010 17:41:27 +0200 |
wenzelm |
renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
|
file |
diff |
annotate
|
| Sat, 15 May 2010 21:41:32 +0200 |
wenzelm |
less pervasive names from structure Thm;
|
file |
diff |
annotate
|
| Wed, 12 May 2010 14:52:23 +0200 |
wenzelm |
do not emit legacy_feature warnings here -- users have no chance to disable them;
|
file |
diff |
annotate
|
| Mon, 03 May 2010 14:25:56 +0200 |
wenzelm |
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
|
file |
diff |
annotate
|
| Sat, 27 Mar 2010 18:07:21 +0100 |
wenzelm |
moved Primitive_Defs.mk_defpair to OldGoals.mk_defpair;
|
file |
diff |
annotate
|
| Sun, 07 Mar 2010 12:19:47 +0100 |
wenzelm |
modernized structure Object_Logic;
|
file |
diff |
annotate
|
| Fri, 19 Feb 2010 20:39:48 +0100 |
wenzelm |
moved ancient Drule.get_def to OldGoals.get_def;
|
file |
diff |
annotate
|
| Sun, 07 Feb 2010 19:33:34 +0100 |
wenzelm |
renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 10:15:31 +0200 |
haftmann |
removed old-style \ and \\ infixes
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 15:57:51 +0200 |
wenzelm |
indicate CRITICAL nature of various setmp combinators;
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 00:52:37 +0200 |
wenzelm |
explicitly qualify Drule.standard;
|
file |
diff |
annotate
|
| Tue, 29 Sep 2009 11:49:22 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
| Fri, 28 Aug 2009 21:04:03 +0200 |
wenzelm |
modernized messages -- eliminated ctyp/cterm operations;
|
file |
diff |
annotate
|
| Mon, 27 Jul 2009 20:45:40 +0200 |
wenzelm |
moved METAHYPS to old_goals.ML (cf. SUBPROOF and FOCUS in subgoal.ML for properly localized versions of the same idea);
|
file |
diff |
annotate
|
| Sat, 25 Jul 2009 10:31:27 +0200 |
wenzelm |
renamed structure Display_Goal to Goal_Display;
|
file |
diff |
annotate
|
| Fri, 24 Jul 2009 22:17:32 +0200 |
wenzelm |
eliminated the_context;
|
file |
diff |
annotate
|
| Fri, 24 Jul 2009 20:55:56 +0200 |
wenzelm |
structure OldGoals: no pervasive names;
|
file |
diff |
annotate
|
| Thu, 23 Jul 2009 16:52:16 +0200 |
wenzelm |
clarified pretty_goals, pretty_thm_aux: plain context;
|
file |
diff |
annotate
|
| Tue, 21 Jul 2009 01:03:18 +0200 |
wenzelm |
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
|
file |
diff |
annotate
|
| Mon, 20 Jul 2009 21:20:09 +0200 |
wenzelm |
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 23:21:44 +0100 |
wenzelm |
removed Ids;
|
file |
diff |
annotate
|
| Sat, 13 Dec 2008 15:00:39 +0100 |
wenzelm |
Context.display_names;
|
file |
diff |
annotate
|
| Mon, 23 Jun 2008 23:45:45 +0200 |
wenzelm |
Logic.is_all;
|
file |
diff |
annotate
|
| Wed, 18 Jun 2008 18:55:04 +0200 |
wenzelm |
added emulations for simple_read_term/read_term/read_prop (formerly in sign.ML);
|
file |
diff |
annotate
|
| Mon, 16 Jun 2008 22:13:49 +0200 |
wenzelm |
removed obsolete no_qed, quick_and_dirty_prove_goalw_cterm;
|
file |
diff |
annotate
|
| Mon, 16 Jun 2008 17:54:47 +0200 |
wenzelm |
removed obsolete inst;
|
file |
diff |
annotate
|
| Wed, 11 Jun 2008 18:03:38 +0200 |
wenzelm |
qualified inst;
|
file |
diff |
annotate
|
| Sun, 18 May 2008 15:04:09 +0200 |
wenzelm |
moved global pretty/string_of functions from Sign to Syntax;
|
file |
diff |
annotate
|