| Sun, 18 Mar 2012 13:04:22 +0100 |
wenzelm |
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 20:22:22 +0200 |
wenzelm |
tuned signature: Name.invent and Name.invent_names;
|
file |
diff |
annotate
|
| Mon, 18 Apr 2011 11:44:39 +0200 |
wenzelm |
pass plain Proof.context for pretty printing;
|
file |
diff |
annotate
|
| Mon, 18 Apr 2011 11:13:29 +0200 |
wenzelm |
simplified pretty printing context, which is only required for certain kernel operations;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 15:25:25 +0200 |
wenzelm |
prefer local name spaces;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 13:48:45 +0200 |
wenzelm |
Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
|
file |
diff |
annotate
|
| Mon, 06 Sep 2010 22:58:06 +0200 |
wenzelm |
turned show_hyps and show_tags into proper configuration option;
|
file |
diff |
annotate
|
| Fri, 03 Sep 2010 21:13:53 +0200 |
wenzelm |
pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
|
file |
diff |
annotate
|
| Fri, 03 Sep 2010 11:21:58 +0200 |
wenzelm |
turned show_consts into proper configuration option;
|
file |
diff |
annotate
|
| Tue, 01 Jun 2010 22:19:17 +0200 |
wenzelm |
arities: no need to maintain original codomain (cf. f795c1164708) -- completion happens in axclass.ML;
|
file |
diff |
annotate
|
| Sun, 25 Apr 2010 21:18:04 +0200 |
wenzelm |
replaced Sorts.rep_algebra by slightly more abstract selectors classes_of/arities_of;
|
file |
diff |
annotate
|
| Sat, 20 Mar 2010 17:33:11 +0100 |
wenzelm |
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
|
file |
diff |
annotate
|
| Thu, 18 Feb 2010 20:44:22 +0100 |
wenzelm |
pretty_full_theory: proper Syntax.init_pretty_global;
|
file |
diff |
annotate
|
| Sun, 25 Oct 2009 21:35:46 +0100 |
wenzelm |
eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
|
file |
diff |
annotate
|
| Sun, 25 Oct 2009 13:18:35 +0100 |
wenzelm |
conceal consts via name space, not tags;
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 19:47:37 +0200 |
wenzelm |
renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 19:20:03 +0200 |
wenzelm |
eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
|
file |
diff |
annotate
|
| Wed, 30 Sep 2009 22:20:58 +0200 |
wenzelm |
eliminated redundant bindings;
|
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:15:22 +0200 |
wenzelm |
discontinued Display.pretty_ctyp/cterm etc.;
|
file |
diff |
annotate
|
| Fri, 28 Aug 2009 18:19:07 +0200 |
wenzelm |
removed obsolete print_ctyp, print_cterm;
|
file |
diff |
annotate
|
| Sat, 25 Jul 2009 10:31:27 +0200 |
wenzelm |
renamed structure Display_Goal to Goal_Display;
|
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 00:56:19 +0200 |
wenzelm |
moved ProofContext.pretty_thm to Display.pretty_thm 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
|
| Thu, 26 Mar 2009 15:18:50 +0100 |
wenzelm |
pretty_thm_aux etc.: explicit show_status flag;
|
file |
diff |
annotate
|
| Tue, 24 Mar 2009 21:24:53 +0100 |
wenzelm |
display derivation status of thms;
|
file |
diff |
annotate
|
| Tue, 10 Mar 2009 16:43:59 +0100 |
wenzelm |
pretty_full_theory: no longer display name prefix -- naming is far more complex now;
|
file |
diff |
annotate
|
| Sun, 01 Mar 2009 14:45:23 +0100 |
wenzelm |
replaced archaic Display.pretty_fact by FindTheorems.pretty_thm, which observes the context properly (as did the former prt_fact already);
|
file |
diff |
annotate
|
| Wed, 11 Feb 2009 16:03:10 +1100 |
kleing |
Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
|
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
|
| Tue, 18 Nov 2008 18:25:45 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 15 Nov 2008 21:31:21 +0100 |
wenzelm |
pretty_thm: oracle flag is always false for now (would require detailed check wrt. promises);
|
file |
diff |
annotate
|
| Mon, 22 Sep 2008 15:26:07 +0200 |
wenzelm |
type thm: fully internal derivation, no longer exported;
|
file |
diff |
annotate
|
| Thu, 18 Sep 2008 19:39:44 +0200 |
wenzelm |
simplified oracle interface;
|
file |
diff |
annotate
|
| Thu, 18 Sep 2008 14:06:56 +0200 |
wenzelm |
added deriv.ML: Abstract derivations based on raw proof terms.
|
file |
diff |
annotate
|
| Fri, 20 Jun 2008 21:00:26 +0200 |
haftmann |
type constructors now with markup
|
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
|
| Sat, 17 May 2008 13:54:30 +0200 |
wenzelm |
structure Display: less pervasive operations;
|
file |
diff |
annotate
|
| Sun, 13 Apr 2008 16:40:02 +0200 |
wenzelm |
tsig: removed unnecessary universal witness;
|
file |
diff |
annotate
|
| Sat, 12 Apr 2008 17:00:35 +0200 |
wenzelm |
rep_cterm/rep_thm: no longer dereference theory_ref;
|
file |
diff |
annotate
|
| Thu, 27 Mar 2008 14:41:07 +0100 |
wenzelm |
removed Display.raw_string_of_XXX (use regular Sign.string_of_XXX);
|
file |
diff |
annotate
|
| Sun, 11 Nov 2007 20:29:05 +0100 |
wenzelm |
simplified Consts.dest;
|
file |
diff |
annotate
|
| Tue, 09 Oct 2007 00:20:13 +0200 |
wenzelm |
generic Syntax.pretty/string_of operations;
|
file |
diff |
annotate
|
| Thu, 04 Oct 2007 20:29:24 +0200 |
wenzelm |
replaced literal 'a by Name.aT;
|
file |
diff |
annotate
|
| Sun, 30 Sep 2007 16:20:35 +0200 |
wenzelm |
print_theory: observe Markup.internal_property of consts, discontinued special treatment of internal names elsewhere;
|
file |
diff |
annotate
|
| Thu, 20 Sep 2007 20:56:33 +0200 |
wenzelm |
avoid Theory.rep_theory;
|
file |
diff |
annotate
|
| Sun, 08 Jul 2007 19:52:05 +0200 |
wenzelm |
thm tag: Markup.property list;
|
file |
diff |
annotate
|
| Sat, 07 Jul 2007 18:39:14 +0200 |
wenzelm |
pretty_goals_aux: subgoal markup;
|
file |
diff |
annotate
|
| Tue, 08 May 2007 21:02:26 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 07 May 2007 00:49:59 +0200 |
wenzelm |
simplified DataFun interfaces;
|
file |
diff |
annotate
|
| Sat, 09 Dec 2006 18:05:40 +0100 |
wenzelm |
abbrevs: print original rhs;
|
file |
diff |
annotate
|
| Tue, 05 Dec 2006 00:30:38 +0100 |
wenzelm |
thm/prf: separate official name vs. additional tags;
|
file |
diff |
annotate
|
| Tue, 19 Sep 2006 23:15:38 +0200 |
wenzelm |
pretty_full_theory: suppress internal entities by default;
|
file |
diff |
annotate
|
| Thu, 27 Jul 2006 13:43:04 +0200 |
wenzelm |
removed obsolete pretty_thm_no_quote;
|
file |
diff |
annotate
|
| Wed, 26 Jul 2006 00:44:49 +0200 |
wenzelm |
moved pprint functions to Isar/proof_display.ML;
|
file |
diff |
annotate
|
| Tue, 11 Jul 2006 12:17:01 +0200 |
wenzelm |
Name.invent_list;
|
file |
diff |
annotate
|
| Wed, 07 Jun 2006 02:01:28 +0200 |
wenzelm |
renamed Type.(un)varifyT to Logic.(un)varifyT;
|
file |
diff |
annotate
|
| Tue, 23 May 2006 14:00:06 +0200 |
wenzelm |
made smlnj happy;
|
file |
diff |
annotate
|