| Wed, 02 Aug 2006 22:26:56 +0200 |
wenzelm |
renamed Syntax.indexname to Syntax.read_indexname;
|
file |
diff |
annotate
|
| Thu, 27 Jul 2006 13:43:10 +0200 |
wenzelm |
removed obsolete is_fact (cf. Thm.no_prems);
|
file |
diff |
annotate
|
| Wed, 26 Jul 2006 19:37:41 +0200 |
wenzelm |
Variable.import(T): result includes fixed types/terms;
|
file |
diff |
annotate
|
| Wed, 12 Jul 2006 21:19:19 +0200 |
wenzelm |
exported make_elim_preserve;
|
file |
diff |
annotate
|
| Mon, 19 Jun 2006 20:21:30 +0200 |
wenzelm |
eliminated freeze/varify in favour of Variable.import/export/trade;
|
file |
diff |
annotate
|
| Mon, 29 May 2006 13:15:53 +0200 |
paulson |
fixing a variable-clash bug in rule_by_tactic
|
file |
diff |
annotate
|
| Tue, 02 May 2006 14:27:49 +0200 |
paulson |
tidied and harmonized "params_of_state"
|
file |
diff |
annotate
|
| Thu, 27 Apr 2006 15:06:35 +0200 |
wenzelm |
tuned basic list operators (flat, maps, map_filter);
|
file |
diff |
annotate
|
| Wed, 26 Apr 2006 22:38:05 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 13 Apr 2006 12:01:01 +0200 |
wenzelm |
use conjunction stuff from conjunction.ML;
|
file |
diff |
annotate
|
| Sat, 04 Mar 2006 21:10:09 +0100 |
wenzelm |
tuned conj_curry;
|
file |
diff |
annotate
|
| Wed, 22 Feb 2006 22:18:39 +0100 |
wenzelm |
simplified Pure conjunction, based on actual const;
|
file |
diff |
annotate
|
| Wed, 15 Feb 2006 21:35:06 +0100 |
wenzelm |
sane version of distinct_subgoals_tac, based on composition with Drule.distinct_prems_rl;
|
file |
diff |
annotate
|
| Wed, 08 Feb 2006 14:39:00 +0100 |
haftmann |
introduced gen_distinct in place of distinct
|
file |
diff |
annotate
|
| Fri, 23 Dec 2005 15:16:49 +0100 |
wenzelm |
CONJUNCTS: full nesting (again), PRECISE_CONJUNCTS: outer level of nesting;
|
file |
diff |
annotate
|
| Thu, 22 Dec 2005 00:29:01 +0100 |
wenzelm |
conjunction_tac: single goal;
|
file |
diff |
annotate
|
| Sat, 19 Nov 2005 14:21:06 +0100 |
wenzelm |
added CONJUNCTS: treat conjunction as separate sub-goals;
|
file |
diff |
annotate
|
| Thu, 10 Nov 2005 20:57:11 +0100 |
wenzelm |
renamed Thm.cgoal_of to Thm.cprem_of;
|
file |
diff |
annotate
|
| Fri, 28 Oct 2005 22:28:03 +0200 |
wenzelm |
accomodate simplified Thm.lift_rule;
|
file |
diff |
annotate
|
| Fri, 21 Oct 2005 18:14:48 +0200 |
wenzelm |
moved norm_hhf_rule, prove etc. to goal.ML;
|
file |
diff |
annotate
|
| Tue, 18 Oct 2005 17:59:25 +0200 |
wenzelm |
Simplifier.theory_context;
|
file |
diff |
annotate
|
| Sat, 15 Oct 2005 00:08:00 +0200 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
| Tue, 20 Sep 2005 08:21:49 +0200 |
haftmann |
slight adaptions to library changes
|
file |
diff |
annotate
|
| Tue, 06 Sep 2005 08:30:43 +0200 |
haftmann |
introduced some new-style AList operations
|
file |
diff |
annotate
|
| Wed, 31 Aug 2005 15:46:40 +0200 |
wenzelm |
refer to theory instead of low-level tsig;
|
file |
diff |
annotate
|
| Thu, 28 Jul 2005 15:19:59 +0200 |
wenzelm |
norm_hhf_rule: Thm.adjust_maxidx_thm before Drule.gen_all;
|
file |
diff |
annotate
|
| Tue, 19 Jul 2005 17:21:47 +0200 |
wenzelm |
Logic.incr_tvar;
|
file |
diff |
annotate
|
| Wed, 13 Jul 2005 16:07:30 +0200 |
wenzelm |
export eq_brl;
|
file |
diff |
annotate
|
| Fri, 01 Jul 2005 22:34:50 +0200 |
wenzelm |
cterm_aconv: avoid rep_cterm;
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 18:33:08 +0200 |
wenzelm |
accomodate identification of type Sign.sg and theory;
|
file |
diff |
annotate
|