| Sun, 01 Mar 2009 23:36:12 +0100 |
wenzelm |
use long names for old-style fold combinators;
|
file |
diff |
annotate
|
| Wed, 31 Dec 2008 00:08:13 +0100 |
wenzelm |
use regular Term.add_vars, Term.add_frees etc.;
|
file |
diff |
annotate
|
| Tue, 28 Oct 2008 11:05:44 +0100 |
paulson |
The metis method no longer fails because the theorem is too trivial
|
file |
diff |
annotate
|
| Wed, 08 Oct 2008 18:09:36 +0200 |
paulson |
The result of the equality inference rule no longer undergoes factoring.
|
file |
diff |
annotate
|
| Wed, 17 Sep 2008 21:27:08 +0200 |
wenzelm |
back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
|
file |
diff |
annotate
|
| Tue, 16 Sep 2008 12:25:04 +0200 |
paulson |
The metis method now fails in the usual manner, rather than raising an exception,
|
file |
diff |
annotate
|
| Tue, 09 Sep 2008 16:17:08 +0200 |
paulson |
Overall exception handler in order to insulate our users from low-level bugs.
|
file |
diff |
annotate
|
| Thu, 14 Aug 2008 16:52:46 +0200 |
wenzelm |
moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
|
file |
diff |
annotate
|
| Mon, 16 Jun 2008 22:13:39 +0200 |
wenzelm |
pervasive RuleInsts;
|
file |
diff |
annotate
|
| Mon, 16 Jun 2008 17:54:43 +0200 |
wenzelm |
RuleInsts.read_instantiate;
|
file |
diff |
annotate
|
| Thu, 12 Jun 2008 18:54:29 +0200 |
wenzelm |
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
|
file |
diff |
annotate
|
| Wed, 11 Jun 2008 18:02:00 +0200 |
wenzelm |
Drule.read_instantiate;
|
file |
diff |
annotate
|
| Sun, 18 May 2008 17:03:20 +0200 |
wenzelm |
eliminated theory CPure;
|
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 15:31:42 +0200 |
wenzelm |
cat_lines;
|
file |
diff |
annotate
|
| Sat, 17 May 2008 13:54:30 +0200 |
wenzelm |
structure Display: less pervasive operations;
|
file |
diff |
annotate
|
| Mon, 07 Apr 2008 15:37:04 +0200 |
paulson |
Superficial changes
|
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
|
| Wed, 02 Jan 2008 12:22:38 +0100 |
paulson |
testing for empty sort
|
file |
diff |
annotate
|
| Thu, 20 Dec 2007 11:16:19 +0100 |
wenzelm |
made refute non-critical (seems to work after avoiding floating point random numbers);
|
file |
diff |
annotate
|
| Wed, 19 Dec 2007 23:06:13 +0100 |
wenzelm |
removed duplicate CRITICAL markup;
|
file |
diff |
annotate
|
| Wed, 19 Dec 2007 17:40:48 +0100 |
paulson |
Replaced refs by config params; finer critical section in mets method
|
file |
diff |
annotate
|
| Wed, 19 Dec 2007 16:52:07 +0100 |
wenzelm |
marked refute (the main metis procedure) as CRITICAL;
|
file |
diff |
annotate
|
| Tue, 18 Dec 2007 17:37:25 +0100 |
paulson |
Deleted redundant setmp calls
|
file |
diff |
annotate
|
| Thu, 11 Oct 2007 16:51:39 +0200 |
paulson |
reconstruction bug fix
|
file |
diff |
annotate
|
| Thu, 11 Oct 2007 15:59:31 +0200 |
paulson |
rationalized redundant code
|
file |
diff |
annotate
|
| Wed, 10 Oct 2007 10:50:11 +0200 |
paulson |
getting rid of type typ_var
|
file |
diff |
annotate
|
| Tue, 09 Oct 2007 18:14:00 +0200 |
paulson |
context-based treatment of generalization; also handling TFrees in axiom clauses
|
file |
diff |
annotate
|
| Tue, 09 Oct 2007 00:20:13 +0200 |
wenzelm |
generic Syntax.pretty/string_of operations;
|
file |
diff |
annotate
|
| Fri, 05 Oct 2007 09:59:21 +0200 |
paulson |
metis method: used theorems
|
file |
diff |
annotate
|
| Thu, 04 Oct 2007 12:32:58 +0200 |
paulson |
combinator translation
|
file |
diff |
annotate
|
| Fri, 31 Aug 2007 18:46:34 +0200 |
wenzelm |
type_infer: mode_pattern;
|
file |
diff |
annotate
|
| Thu, 30 Aug 2007 22:35:38 +0200 |
wenzelm |
replaced ProofContext.infer_types by general Syntax.check_terms;
|
file |
diff |
annotate
|
| Fri, 24 Aug 2007 14:15:58 +0200 |
paulson |
Reconstruction bug fix
|
file |
diff |
annotate
|
| Sat, 18 Aug 2007 13:32:20 +0200 |
wenzelm |
export more tactics;
|
file |
diff |
annotate
|
| Fri, 17 Aug 2007 23:10:39 +0200 |
wenzelm |
turned type_lits into configuration option (with attribute);
|
file |
diff |
annotate
|
| Fri, 17 Aug 2007 00:03:50 +0200 |
wenzelm |
proper signature for Meson;
|
file |
diff |
annotate
|
| Sun, 29 Jul 2007 14:29:57 +0200 |
wenzelm |
metis_tac: proper context (ProofContext.init it *not* sufficient);
|
file |
diff |
annotate
|
| Wed, 20 Jun 2007 23:19:18 +0200 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
| Wed, 20 Jun 2007 22:07:52 +0200 |
wenzelm |
The Metis prover (slightly modified version from Larry);
|
file |
diff |
annotate
|