| Mon, 17 May 2010 23:54:15 +0200 |
wenzelm |
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
|
file |
diff |
annotate
|
| Mon, 10 May 2010 20:53:06 +0200 |
wenzelm |
renamed Config.get_thy to Config.get_global etc. to indicate that this is not the real thing;
|
file |
diff |
annotate
|
| Sun, 28 Mar 2010 16:59:06 +0200 |
wenzelm |
static defaults for configuration options;
|
file |
diff |
annotate
|
| Sun, 07 Mar 2010 12:19:47 +0100 |
wenzelm |
modernized structure Object_Logic;
|
file |
diff |
annotate
|
| Sat, 06 Mar 2010 15:39:16 +0100 |
wenzelm |
eliminated Args.bang_facts (legacy feature);
|
file |
diff |
annotate
|
| Sun, 01 Nov 2009 15:44:26 +0100 |
wenzelm |
modernized structure Context_Rules;
|
file |
diff |
annotate
|
| 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
|
| Fri, 10 Nov 2006 23:22:01 +0100 |
wenzelm |
tuned names of start_timing,/end_timing/check_timer;
|
file |
diff |
annotate
|
| Wed, 04 Oct 2006 14:17:38 +0200 |
haftmann |
insert replacing ins ins_int ins_string
|
file |
diff |
annotate
|
| Thu, 21 Sep 2006 19:04:20 +0200 |
wenzelm |
member (op =);
|
file |
diff |
annotate
|
| Sat, 29 Apr 2006 23:16:43 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 27 Apr 2006 15:06:35 +0200 |
wenzelm |
tuned basic list operators (flat, maps, map_filter);
|
file |
diff |
annotate
|
| Tue, 14 Feb 2006 13:03:00 +0100 |
paulson |
fixed tracing
|
file |
diff |
annotate
|
| Thu, 19 Jan 2006 21:22:08 +0100 |
wenzelm |
setup: theory -> theory;
|
file |
diff |
annotate
|
| Sat, 31 Dec 2005 21:49:41 +0100 |
wenzelm |
explicitly reject consts *Goal*, *False*;
|
file |
diff |
annotate
|
| Fri, 30 Dec 2005 16:56:59 +0100 |
wenzelm |
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
|
file |
diff |
annotate
|
| Wed, 16 Nov 2005 17:45:23 +0100 |
wenzelm |
Trueprop: use ObjectLogic.judgment etc.;
|
file |
diff |
annotate
|
| Mon, 14 Nov 2005 18:25:34 +0100 |
paulson |
removal of is_hol
|
file |
diff |
annotate
|
| Thu, 10 Nov 2005 20:57:16 +0100 |
wenzelm |
uncurried Consts.typargs;
|
file |
diff |
annotate
|
| Wed, 02 Nov 2005 14:46:53 +0100 |
wenzelm |
fromConst: use Sign.const_typargs for efficient representation of type instances of constant declarations;
|
file |
diff |
annotate
|
| Thu, 27 Oct 2005 13:54:40 +0200 |
wenzelm |
replaced Defs.monomorphic by Sign.monomorphic;
|
file |
diff |
annotate
|
| Sat, 08 Oct 2005 20:15:34 +0200 |
wenzelm |
minor tweaks for Poplog/PML;
|
file |
diff |
annotate
|
| Tue, 06 Sep 2005 08:30:43 +0200 |
haftmann |
introduced some new-style AList operations
|
file |
diff |
annotate
|
| Mon, 05 Sep 2005 08:14:35 +0200 |
haftmann |
introduced binding priority 1 for linear combinators etc.
|
file |
diff |
annotate
|
| Mon, 01 Aug 2005 19:20:30 +0200 |
wenzelm |
Defs.monomorphic;
|
file |
diff |
annotate
|
| Fri, 15 Jul 2005 15:35:28 +0200 |
obua |
optimize no_types_needed, remove exception handler
|
file |
diff |
annotate
|
| Tue, 12 Jul 2005 12:49:46 +0200 |
paulson |
experimental code to reduce the amount of type information in blast
|
file |
diff |
annotate
|
| Wed, 20 Apr 2005 22:43:52 +0200 |
gagern |
Added op in front of constructor for better parsing.
|
file |
diff |
annotate
|
| Thu, 07 Apr 2005 09:25:33 +0200 |
wenzelm |
reverted renaming of Some/None in comments and strings;
|
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
|
| Sun, 29 Aug 2004 17:36:39 +0200 |
webertj |
depth limit (previously hard-coded with a value of 20) made a reference
|
file |
diff |
annotate
|
| Mon, 21 Jun 2004 16:39:39 +0200 |
wenzelm |
immediate_output;
|
file |
diff |
annotate
|
| Wed, 09 Jun 2004 18:57:18 +0200 |
wenzelm |
prs: Output.output;
|
file |
diff |
annotate
|
| Mon, 15 Mar 2004 10:45:31 +0100 |
paulson |
more up-to-date error msg
|
file |
diff |
annotate
|
| Fri, 30 Aug 2002 16:42:45 +0200 |
paulson |
removal of blast.overloaded
|
file |
diff |
annotate
|
| Wed, 20 Feb 2002 00:53:53 +0100 |
wenzelm |
Symbol.bump_string;
|
file |
diff |
annotate
|
| Thu, 06 Dec 2001 00:42:24 +0100 |
wenzelm |
tuned xtra_netpair;
|
file |
diff |
annotate
|
| Wed, 05 Dec 2001 03:06:05 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 03 Dec 2001 21:01:37 +0100 |
wenzelm |
removed questionable init_gensym;
|
file |
diff |
annotate
|
| Mon, 15 Oct 2001 20:36:04 +0200 |
wenzelm |
Tactic.orderlist;
|
file |
diff |
annotate
|
| Sun, 14 Oct 2001 20:04:05 +0200 |
wenzelm |
ObjectLogic.atomize_tac;
|
file |
diff |
annotate
|
| Fri, 16 Feb 2001 13:29:07 +0100 |
paulson |
Blast bug fix: now always duplicates when applying a haz rule,
|
file |
diff |
annotate
|
| Wed, 14 Feb 2001 13:26:46 +0100 |
paulson |
new function get_overloads
|
file |
diff |
annotate
|
| Mon, 06 Nov 2000 22:47:41 +0100 |
wenzelm |
tuned atomize_goal;
|
file |
diff |
annotate
|
| Fri, 01 Sep 2000 00:36:08 +0200 |
wenzelm |
Method.bang_sectioned_args';
|
file |
diff |
annotate
|
| Tue, 01 Aug 2000 11:57:09 +0200 |
wenzelm |
handle actual object-logic rules by atomizing the goal;
|
file |
diff |
annotate
|
| Wed, 28 Jun 2000 10:54:47 +0200 |
paulson |
warns of weak elim rules and ignores them
|
file |
diff |
annotate
|
| Sat, 25 Sep 1999 13:23:58 +0200 |
wenzelm |
simplified sectioned_args;
|
file |
diff |
annotate
|
| Tue, 21 Sep 1999 17:26:50 +0200 |
wenzelm |
setup for refined facts handling;
|
file |
diff |
annotate
|
| Wed, 18 Aug 1999 20:47:31 +0200 |
wenzelm |
Method.modifier;
|
file |
diff |
annotate
|
| Mon, 02 Aug 1999 17:59:25 +0200 |
wenzelm |
blast method: optional depth argument;
|
file |
diff |
annotate
|
| Wed, 14 Jul 1999 13:05:46 +0200 |
wenzelm |
improved comment;
|
file |
diff |
annotate
|
| Fri, 09 Jul 1999 18:54:55 +0200 |
wenzelm |
type claset: added extra I/E rules;
|
file |
diff |
annotate
|
| Wed, 17 Mar 1999 16:33:47 +0100 |
wenzelm |
Theory.sign_of;
|
file |
diff |
annotate
|
| Wed, 25 Nov 1998 14:03:20 +0100 |
wenzelm |
replaced prs by std_output / writeln;
|
file |
diff |
annotate
|
| Wed, 18 Nov 1998 11:01:48 +0100 |
wenzelm |
method setup;
|
file |
diff |
annotate
|
| Fri, 23 Oct 1998 11:03:35 +0200 |
paulson |
occurs check now handles Bound variables (for soundness)
|
file |
diff |
annotate
|
| Mon, 05 Oct 1998 10:30:57 +0200 |
paulson |
MLWorks demands the "op" before $
|
file |
diff |
annotate
|
| Fri, 11 Sep 1998 16:31:40 +0200 |
paulson |
Less deterministic reconstruction: now more robust but perhaps slower
|
file |
diff |
annotate
|
| Thu, 10 Sep 1998 17:33:09 +0200 |
paulson |
Allows more backtracking in proof reconstruction, making it slower but more
|
file |
diff |
annotate
|
| Tue, 01 Sep 1998 10:10:27 +0200 |
paulson |
fixed error msg
|
file |
diff |
annotate
|
| Wed, 19 Aug 1998 10:49:30 +0200 |
paulson |
new version, more resistant to PROOF FAILED. Now it distinguishes between
|
file |
diff |
annotate
|
| Wed, 25 Feb 1998 20:29:58 +0100 |
oheimb |
renamed rep_claset to rep_cs
|
file |
diff |
annotate
|
| Wed, 25 Feb 1998 15:51:24 +0100 |
oheimb |
changed wrapper mechanism of classical reasoner
|
file |
diff |
annotate
|
| Fri, 02 Jan 1998 17:16:39 +0100 |
paulson |
Blast_tac now squashes flex-flex pairs immediately
|
file |
diff |
annotate
|
| Tue, 23 Dec 1997 11:39:03 +0100 |
paulson |
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
|
file |
diff |
annotate
|
| Fri, 12 Dec 1997 10:34:21 +0100 |
paulson |
More deterministic and therefore faster (sometimes) proof reconstruction
|
file |
diff |
annotate
|
| Wed, 03 Dec 1997 11:42:45 +0100 |
paulson |
Fixed the treatment of substitution for equations, restricting occurrences of
|
file |
diff |
annotate
|
| Fri, 28 Nov 1997 10:52:04 +0100 |
paulson |
Printing of statistics including time for search & reconstruction
|
file |
diff |
annotate
|
| Wed, 26 Nov 1997 16:49:54 +0100 |
paulson |
Statistics
|
file |
diff |
annotate
|
| Fri, 21 Nov 1997 15:29:56 +0100 |
wenzelm |
changed Pure/Sequence interface -- isatool fixseq;
|
file |
diff |
annotate
|
| Thu, 20 Nov 1997 10:54:04 +0100 |
paulson |
Renamed "overload" to "overloaded" for sml/nj compatibility
|
file |
diff |
annotate
|
| Mon, 17 Nov 1997 10:48:07 +0100 |
paulson |
Rationalized error handling: if low-level tactic (depth_tac) cannot accept the
|
file |
diff |
annotate
|
| Tue, 11 Nov 1997 11:12:37 +0100 |
paulson |
Now applies "map negOfGoal" to lits when expanding haz rules.
|
file |
diff |
annotate
|
| Wed, 05 Nov 1997 11:45:51 +0100 |
wenzelm |
fixed exception OPTION;
|
file |
diff |
annotate
|
| Mon, 03 Nov 1997 11:56:17 +0100 |
wenzelm |
adapted to new implicit claset mechanism;
|
file |
diff |
annotate
|
| Sat, 01 Nov 1997 13:02:39 +0100 |
paulson |
New treatment of overloading\!
|
file |
diff |
annotate
|
| Fri, 17 Oct 1997 11:12:36 +0200 |
paulson |
A lot of new comments
|
file |
diff |
annotate
|
| Fri, 18 Jul 1997 13:54:41 +0200 |
wenzelm |
tuned warning;
|
file |
diff |
annotate
|
| Thu, 19 Jun 1997 11:31:14 +0200 |
paulson |
Made proofs more concise by replacing calls to spy_analz_tac by uses of
|
file |
diff |
annotate
|
| Tue, 20 May 1997 11:47:33 +0200 |
paulson |
Basis library version of type "option" now resides in its own structure Option
|
file |
diff |
annotate
|
| Mon, 05 May 1997 12:15:20 +0200 |
paulson |
Again "norm" DOES NOT normalize bodies of abstractions
|
file |
diff |
annotate
|
| Fri, 02 May 1997 10:18:50 +0200 |
paulson |
More tracing. hyp_subst_tac allowed to fail
|
file |
diff |
annotate
|
| Wed, 30 Apr 1997 12:59:24 +0200 |
paulson |
More tracing; less exception handling
|
file |
diff |
annotate
|
| Thu, 24 Apr 1997 19:47:53 +0200 |
wenzelm |
refer to SOME, NONE on top-level;
|
file |
diff |
annotate
|
| Thu, 24 Apr 1997 11:21:46 +0200 |
paulson |
Addition of printed tracing. Also some tidying
|
file |
diff |
annotate
|
| Wed, 23 Apr 1997 11:11:38 +0200 |
paulson |
Loop detection: before expanding a haz formula, see whether it is a duplicate
|
file |
diff |
annotate
|
| Mon, 21 Apr 1997 10:16:01 +0200 |
paulson |
Penalty for branching instantiations reduced from log3 to log4.
|
file |
diff |
annotate
|
| Tue, 15 Apr 1997 10:22:50 +0200 |
paulson |
Changed penalty from log2 to log3
|
file |
diff |
annotate
|