| Tue, 29 Sep 2009 16:24:36 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
| Fri, 24 Jul 2009 21:21:45 +0200 |
wenzelm |
renamed functor BlastFun to Blast, require explicit theory;
|
file |
diff |
annotate
|
| Fri, 24 Jul 2009 21:02:34 +0200 |
wenzelm |
explicit OldGoals;
|
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, 06 Jul 2009 21:24:30 +0200 |
wenzelm |
structure Thm: less pervasive names;
|
file |
diff |
annotate
|
| Thu, 26 Mar 2009 14:14:02 +0100 |
wenzelm |
simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
|
file |
diff |
annotate
|
| Fri, 20 Mar 2009 17:12:37 +0100 |
wenzelm |
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
|
file |
diff |
annotate
|
| Tue, 17 Mar 2009 14:09:20 +0100 |
wenzelm |
renamed Tactic.taglist/untaglist/orderlist to tag_list/untag_list/order_list (in library.ML);
|
file |
diff |
annotate
|
| Sun, 15 Mar 2009 20:25:58 +0100 |
wenzelm |
simplified method setup;
|
file |
diff |
annotate
|
| Fri, 13 Mar 2009 21:25:15 +0100 |
wenzelm |
eliminated type Args.T;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2009 22:50:30 +0100 |
wenzelm |
eliminated Output.immediate_output -- violates the official message channel protocol;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 11:05:29 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 10:45:52 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Sun, 01 Mar 2009 23:36:12 +0100 |
wenzelm |
use long names for old-style fold combinators;
|
file |
diff |
annotate
|
| Sun, 01 Mar 2009 16:21:33 +0100 |
wenzelm |
end_timing: generalized result -- message plus with explicit time values;
|
file |
diff |
annotate
|
| Sat, 09 Aug 2008 22:43:46 +0200 |
wenzelm |
unified Args.T with OuterLex.token, renamed some operations;
|
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 23:53:20 +0200 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
| Sat, 17 May 2008 13:54:30 +0200 |
wenzelm |
structure Display: less pervasive operations;
|
file |
diff |
annotate
|
| Fri, 09 Nov 2007 19:37:35 +0100 |
wenzelm |
avoid obsolete Sign.read_prop;
|
file |
diff |
annotate
|
| Wed, 01 Aug 2007 16:55:40 +0200 |
wenzelm |
simplified internal Config interface;
|
file |
diff |
annotate
|
| Tue, 31 Jul 2007 21:19:21 +0200 |
wenzelm |
replaced depth_limit ref by blast_depth_limit configuration option;
|
file |
diff |
annotate
|
| Sun, 29 Jul 2007 19:46:03 +0200 |
wenzelm |
explicit global state argument -- no longer CRITICAL;
|
file |
diff |
annotate
|
| Wed, 25 Jul 2007 22:20:47 +0200 |
wenzelm |
NAMED_CRITICAL;
|
file |
diff |
annotate
|
| Tue, 24 Jul 2007 19:44:29 +0200 |
wenzelm |
marked some CRITICAL sections;
|
file |
diff |
annotate
|
| Sun, 22 Jul 2007 21:20:53 +0200 |
wenzelm |
blast_hyp_subst_tac: plain bool argument;
|
file |
diff |
annotate
|
| Thu, 05 Jul 2007 20:01:28 +0200 |
wenzelm |
simplified ObjectLogic.atomize;
|
file |
diff |
annotate
|
| Sat, 14 Apr 2007 17:36:05 +0200 |
wenzelm |
Term.string_of_vname;
|
file |
diff |
annotate
|
| Wed, 04 Apr 2007 23:29:33 +0200 |
wenzelm |
rep_thm/cterm/ctyp: removed obsolete sign field;
|
file |
diff |
annotate
|
| Wed, 04 Apr 2007 00:11:10 +0200 |
wenzelm |
cleaned-up Output functions;
|
file |
diff |
annotate
|