| 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
|
| Tue, 23 May 2006 13:55:02 +0200 |
wenzelm |
pretty_full_theory: tuned output of definitions;
|
file |
diff |
annotate
|
| Mon, 22 May 2006 22:29:16 +0200 |
wenzelm |
pretty_full_theory: defs;
|
file |
diff |
annotate
|
| Tue, 16 May 2006 13:01:24 +0200 |
wenzelm |
more abstract interface to classes/arities;
|
file |
diff |
annotate
|
| Mon, 08 May 2006 17:40:07 +0200 |
wenzelm |
added raw_string_of_sort/typ/term;
|
file |
diff |
annotate
|
| Mon, 01 May 2006 17:05:09 +0200 |
wenzelm |
adapted arities;
|
file |
diff |
annotate
|
| Thu, 27 Apr 2006 15:06:35 +0200 |
wenzelm |
tuned basic list operators (flat, maps, map_filter);
|
file |
diff |
annotate
|
| Thu, 13 Apr 2006 12:00:58 +0200 |
wenzelm |
tuned comment;
|
file |
diff |
annotate
|
| Sat, 08 Apr 2006 22:51:19 +0200 |
wenzelm |
print_theory: print abbreviations nicely;
|
file |
diff |
annotate
|
| Tue, 21 Mar 2006 12:18:07 +0100 |
wenzelm |
subtract (op =);
|
file |
diff |
annotate
|
| Wed, 08 Feb 2006 17:15:27 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 06 Feb 2006 20:59:03 +0100 |
wenzelm |
print_theory: const abbreviations;
|
file |
diff |
annotate
|
| Wed, 02 Nov 2005 14:46:57 +0100 |
wenzelm |
Consts.dest;
|
file |
diff |
annotate
|
| Thu, 27 Oct 2005 13:54:43 +0200 |
wenzelm |
consts: monomorphic;
|
file |
diff |
annotate
|
| Thu, 29 Sep 2005 00:58:57 +0200 |
wenzelm |
print_theory: discontinued final consts;
|
file |
diff |
annotate
|
| Sat, 17 Sep 2005 19:17:34 +0200 |
wenzelm |
pretty_thm_aux: ora masked by quick_and_dirty;
|
file |
diff |
annotate
|
| Sat, 17 Sep 2005 18:11:28 +0200 |
wenzelm |
pretty_thm_aux: aconv hyps;
|
file |
diff |
annotate
|
| Sat, 17 Sep 2005 12:18:03 +0200 |
wenzelm |
pretty_thm_aux: observe asms context;
|
file |
diff |
annotate
|
| Thu, 28 Jul 2005 15:19:54 +0200 |
wenzelm |
print_theory: const constraints;
|
file |
diff |
annotate
|
| Thu, 14 Jul 2005 19:28:28 +0200 |
wenzelm |
NameSpace.dest_table avoids duplicated extern;
|
file |
diff |
annotate
|
| Wed, 22 Jun 2005 19:41:19 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 20 Jun 2005 22:14:04 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 18:33:22 +0200 |
wenzelm |
removed pretty_theory, pprint_theory (see context.ML or thy_info.ML);
|
file |
diff |
annotate
|
| Sat, 11 Jun 2005 22:15:48 +0200 |
wenzelm |
refer to name spaces values instead of names;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2005 12:03:21 +0200 |
wenzelm |
print_theory: omit name spaces; NameSpace.extern_table;
|
file |
diff |
annotate
|
| Sun, 05 Jun 2005 23:07:28 +0200 |
wenzelm |
renamed const_deps to defs;
|
file |
diff |
annotate
|
| Tue, 31 May 2005 19:32:41 +0200 |
obua |
Removed final_consts from theory data. Now const_deps deals with final
|
file |
diff |
annotate
|
| Tue, 31 May 2005 11:53:18 +0200 |
wenzelm |
renamed cond_extern to extern;
|
file |
diff |
annotate
|
| Fri, 04 Mar 2005 15:07:34 +0100 |
skalberg |
Removed practically all references to Library.foldr.
|
file |
diff |
annotate
|
| Thu, 03 Mar 2005 12:43:01 +0100 |
skalberg |
Move towards standard functions.
|
file |
diff |
annotate
|
| Sun, 13 Feb 2005 17:15:14 +0100 |
skalberg |
Deleted Library.option type.
|
file |
diff |
annotate
|
| Wed, 23 Jun 2004 09:09:18 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 22 Jun 2004 09:52:08 +0200 |
wenzelm |
improved print_theory;
|
file |
diff |
annotate
|
| Mon, 21 Jun 2004 16:41:06 +0200 |
wenzelm |
pretty_abbr;
|
file |
diff |
annotate
|
| Sat, 05 Jun 2004 13:08:53 +0200 |
wenzelm |
pretty_thm/goals_aux, pretty_flexpair: pp;
|
file |
diff |
annotate
|
| Fri, 21 May 2004 21:28:14 +0200 |
wenzelm |
adapted tsig/sg interface;
|
file |
diff |
annotate
|
| Thu, 22 Apr 2004 10:55:02 +0200 |
wenzelm |
adapted Sign.rep_sg;
|
file |
diff |
annotate
|
| Fri, 16 Apr 2004 18:45:56 +0200 |
berghofe |
Replaced quote by Library.quote, since quote now refers to Symbol.quote
|
file |
diff |
annotate
|
| Fri, 19 Mar 2004 10:42:38 +0100 |
paulson |
Removing the datatype declaration of "order" allows the standard General.order
|
file |
diff |
annotate
|
| Thu, 09 Oct 2003 18:13:32 +0200 |
skalberg |
Added support for making constants final, that is, ensuring that no
|
file |
diff |
annotate
|
| Sun, 31 Aug 2003 21:27:58 +0200 |
skalberg |
Makes interactive proof scripting recognize the show_all_types flag.
|
file |
diff |
annotate
|
| Mon, 21 Oct 2002 17:04:47 +0200 |
berghofe |
Changed handling of flex-flex constraints: now stored in separate
|
file |
diff |
annotate
|
| Mon, 21 Jan 2002 17:02:52 +0100 |
wenzelm |
reset show_hyps by default (in accordance to existing Isar practice);
|
file |
diff |
annotate
|
| Sat, 08 Dec 2001 14:41:36 +0100 |
wenzelm |
tuned print_goals interfaces;
|
file |
diff |
annotate
|
| Tue, 06 Nov 2001 23:52:23 +0100 |
wenzelm |
added goals_limit (from tctical.ML);
|
file |
diff |
annotate
|
| Tue, 06 Nov 2001 19:25:24 +0100 |
wenzelm |
export pretty_thm_aux;
|
file |
diff |
annotate
|
| Mon, 22 Oct 2001 17:59:39 +0200 |
wenzelm |
print_goals stuff is back (from locale.ML);
|
file |
diff |
annotate
|
| Wed, 15 Aug 2001 22:20:30 +0200 |
wenzelm |
support for absolute namespace entry paths;
|
file |
diff |
annotate
|
| Sat, 23 Dec 2000 22:52:41 +0100 |
wenzelm |
tuned output;
|
file |
diff |
annotate
|
| Sun, 17 Sep 2000 22:23:48 +0200 |
wenzelm |
added print_thm(s)_sg;
|
file |
diff |
annotate
|
| Wed, 02 Aug 2000 19:38:33 +0200 |
wenzelm |
use oracle flag from derivation;
|
file |
diff |
annotate
|
| Mon, 22 May 2000 11:57:27 +0200 |
wenzelm |
show_consts no longer requires show_types;
|
file |
diff |
annotate
|
| Mon, 17 Apr 2000 13:57:55 +0200 |
wenzelm |
Pretty.chunks;
|
file |
diff |
annotate
|
| Wed, 15 Mar 2000 18:20:52 +0100 |
wenzelm |
removed Pretty.spc;
|
file |
diff |
annotate
|
| Thu, 09 Mar 2000 22:57:39 +0100 |
wenzelm |
quote tag arguments;
|
file |
diff |
annotate
|
| Wed, 29 Sep 1999 13:50:26 +0200 |
wenzelm |
new tsig components;
|
file |
diff |
annotate
|
| Fri, 23 Jul 1999 16:50:55 +0200 |
wenzelm |
replace assoc lists by Symtab.table;
|
file |
diff |
annotate
|
| Mon, 12 Jul 1999 22:23:07 +0200 |
wenzelm |
removed pretty_thm_no_hyps (again);
|
file |
diff |
annotate
|
| Thu, 08 Jul 1999 18:29:07 +0200 |
wenzelm |
added pretty_thm_no_hyps;
|
file |
diff |
annotate
|
| Sat, 03 Jul 1999 00:40:57 +0200 |
wenzelm |
oops;
|
file |
diff |
annotate
|
| Sat, 03 Jul 1999 00:21:35 +0200 |
wenzelm |
pretty_thm: include oracles (!) in hyps;
|
file |
diff |
annotate
|
| Mon, 28 Jun 1999 21:41:02 +0200 |
wenzelm |
cond_extern_table;
|
file |
diff |
annotate
|
| Wed, 17 Mar 1999 16:33:00 +0100 |
wenzelm |
qualify Theory.sign_of etc.;
|
file |
diff |
annotate
|
| Tue, 09 Mar 1999 12:07:52 +0100 |
wenzelm |
pretty_thm_no_quote;
|
file |
diff |
annotate
|
| Fri, 12 Feb 1999 13:55:54 +0100 |
wenzelm |
pretty_thm: quote terms (separately);
|
file |
diff |
annotate
|
| Tue, 12 Jan 1999 13:14:22 +0100 |
wenzelm |
show_tags;
|
file |
diff |
annotate
|
| Tue, 17 Nov 1998 14:04:52 +0100 |
wenzelm |
Pretty.spc;
|
file |
diff |
annotate
|
| Tue, 04 Aug 1998 18:21:20 +0200 |
wenzelm |
moved print_goals to locale.ML;
|
file |
diff |
annotate
|
| Fri, 05 Jun 1998 14:23:07 +0200 |
wenzelm |
print_data moved to theory.ML;
|
file |
diff |
annotate
|
| Wed, 20 May 1998 18:56:00 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 03 Apr 1998 14:36:20 +0200 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
| Mon, 29 Dec 1997 14:31:20 +0100 |
wenzelm |
pretty_name_space;
|
file |
diff |
annotate
|
| Fri, 19 Dec 1997 10:13:47 +0100 |
wenzelm |
adapted to new sort function;
|
file |
diff |
annotate
|
| Fri, 21 Nov 1997 15:27:43 +0100 |
wenzelm |
changed Sequence interface (now Seq, in seq.ML);
|
file |
diff |
annotate
|
| Thu, 20 Nov 1997 15:28:48 +0100 |
wenzelm |
removed data.ML (made part of sign.ML);
|
file |
diff |
annotate
|
| Thu, 20 Nov 1997 12:51:31 +0100 |
wenzelm |
moved Sign.print_sg to display.ML;
|
file |
diff |
annotate
|
| Wed, 12 Nov 1997 16:21:15 +0100 |
wenzelm |
tuned prths;
|
file |
diff |
annotate
|
| Tue, 04 Nov 1997 16:46:02 +0100 |
wenzelm |
added pretty_ctyp;
|
file |
diff |
annotate
|