| Wed, 31 Dec 2008 15:30:10 +0100 |
wenzelm |
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
|
file |
diff |
annotate
|
| Tue, 10 Jun 2008 16:43:01 +0200 |
wenzelm |
eliminated obsolete case_split_thm -- use case_split;
|
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
|
| Thu, 05 Jul 2007 20:01:26 +0200 |
wenzelm |
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
|
file |
diff |
annotate
|
| Tue, 03 Jul 2007 17:17:07 +0200 |
wenzelm |
Conjunction.intr/elim_balanced;
|
file |
diff |
annotate
|
| Thu, 10 May 2007 00:39:45 +0200 |
wenzelm |
moved conversions to structure Conv;
|
file |
diff |
annotate
|
| Mon, 11 Dec 2006 16:58:19 +0100 |
webertj |
ordered lists instead of tables for resolving hyps; speedup
|
file |
diff |
annotate
|
| Sun, 10 Dec 2006 19:37:27 +0100 |
wenzelm |
ML_Syntax.print_XXX;
|
file |
diff |
annotate
|
| Wed, 29 Nov 2006 13:59:52 +0100 |
webertj |
clauses sorted according to term order (significant speedup in some cases)
|
file |
diff |
annotate
|
| Thu, 23 Nov 2006 00:51:51 +0100 |
wenzelm |
renamed string_of_pair/list/option to ML_Syntax.str_of_pair/list/option;
|
file |
diff |
annotate
|
| Thu, 09 Nov 2006 18:58:52 +0100 |
webertj |
timing/tracing code removed
|
file |
diff |
annotate
|
| Thu, 09 Nov 2006 18:48:45 +0100 |
webertj |
interpreters for fst and snd added
|
file |
diff |
annotate
|
| Wed, 06 Sep 2006 17:39:52 +0200 |
webertj |
rawsat_thm: mk_conjunction_list replaced by Conjunction.mk_conjunction_list
|
file |
diff |
annotate
|
| Sat, 02 Sep 2006 03:10:27 +0200 |
webertj |
tuned
|
file |
diff |
annotate
|
| Wed, 30 Aug 2006 16:27:53 +0200 |
webertj |
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
|
file |
diff |
annotate
|
| Wed, 09 Aug 2006 15:48:51 +0200 |
webertj |
tuned: string_of_list, string_of_pair
|
file |
diff |
annotate
|
| Wed, 02 Aug 2006 00:57:41 +0200 |
webertj |
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
|
file |
diff |
annotate
|
| Thu, 20 Jul 2006 14:34:57 +0200 |
webertj |
comments fixed, member function renamed
|
file |
diff |
annotate
|
| Mon, 10 Jul 2006 21:02:29 +0200 |
webertj |
minor optimization wrt. certifying terms
|
file |
diff |
annotate
|
| Fri, 07 Jul 2006 18:13:58 +0200 |
webertj |
"solver" reference added to make the SAT solver configurable
|
file |
diff |
annotate
|
| Mon, 03 Jul 2006 17:27:09 +0200 |
webertj |
comments fixed, minor optimization wrt. certifying terms
|
file |
diff |
annotate
|
| Wed, 03 May 2006 12:05:53 +0200 |
webertj |
pre_cnf_tac: beta-eta-normalization restricted to the current subgoal
|
file |
diff |
annotate
|
| Tue, 02 May 2006 19:23:48 +0200 |
webertj |
beta_eta_conversion added to pre_cnf_tac
|
file |
diff |
annotate
|
| Fri, 10 Mar 2006 16:31:50 +0100 |
webertj |
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
|
file |
diff |
annotate
|
| Wed, 12 Oct 2005 18:17:48 +0200 |
webertj |
counter added to SAT signature
|
file |
diff |
annotate
|
| Wed, 12 Oct 2005 17:06:22 +0200 |
webertj |
no proof reconstruction when quick_and_dirty is set
|
file |
diff |
annotate
|
| Sun, 09 Oct 2005 17:06:03 +0200 |
webertj |
Tactics sat and satx reimplemented, several improvements
|
file |
diff |
annotate
|
| Wed, 28 Sep 2005 14:41:43 +0200 |
webertj |
pre_sat_tac moved towards end of file
|
file |
diff |
annotate
|
| Wed, 28 Sep 2005 14:16:12 +0200 |
webertj |
comment fixed
|
file |
diff |
annotate
|
| Sat, 24 Sep 2005 07:57:50 +0200 |
webertj |
replay_proof optimized: now performs backwards proof search
|
file |
diff |
annotate
|
| Sat, 24 Sep 2005 07:21:46 +0200 |
webertj |
code reformatted and restructured, many minor modifications
|
file |
diff |
annotate
|
| Fri, 23 Sep 2005 22:58:50 +0200 |
webertj |
new sat tactic imports resolution proofs from zChaff
|
file |
diff |
annotate
|