| Tue, 03 Mar 2009 14:07:23 +0100 |
wenzelm |
added type binding and val empty_binding;
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 16:47:04 +0100 |
haftmann |
binding replaces bstring
|
file |
diff |
annotate
|
| Wed, 31 Dec 2008 15:30:10 +0100 |
wenzelm |
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
|
file |
diff |
annotate
|
| Thu, 04 Dec 2008 14:43:33 +0100 |
haftmann |
cleaned up binding module and related code
|
file |
diff |
annotate
|
| Thu, 23 Oct 2008 15:28:01 +0200 |
wenzelm |
renamed Thm.get_axiom_i to Thm.axiom;
|
file |
diff |
annotate
|
| Thu, 16 Oct 2008 22:44:30 +0200 |
wenzelm |
added check_shyps, which reject pending sort hypotheses;
|
file |
diff |
annotate
|
| Wed, 03 Sep 2008 17:50:37 +0200 |
wenzelm |
simplified add_axiom: no hyps;
|
file |
diff |
annotate
|
| Wed, 27 Aug 2008 11:48:54 +0200 |
wenzelm |
type Properties.T;
|
file |
diff |
annotate
|
| Thu, 14 Aug 2008 16:52:51 +0200 |
wenzelm |
moved basic thm operations from structure PureThy to Thm;
|
file |
diff |
annotate
|
| Wed, 18 Jun 2008 18:55:03 +0200 |
wenzelm |
removed obsolete read_def_cterms/read_cterm;
|
file |
diff |
annotate
|
| Tue, 15 Apr 2008 18:49:19 +0200 |
wenzelm |
Theory.eq_thy;
|
file |
diff |
annotate
|
| Tue, 15 Apr 2008 16:12:05 +0200 |
wenzelm |
Thm.forall_elim_var(s);
|
file |
diff |
annotate
|
| Sat, 12 Apr 2008 17:00:40 +0200 |
wenzelm |
replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);
|
file |
diff |
annotate
|
| Mon, 03 Dec 2007 16:04:16 +0100 |
haftmann |
interface for unchecked definitions
|
file |
diff |
annotate
|
| Thu, 11 Oct 2007 19:10:22 +0200 |
wenzelm |
added elim_implies (more convenient argument order);
|
file |
diff |
annotate
|
| Wed, 10 Oct 2007 17:31:55 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 30 Sep 2007 16:20:37 +0200 |
wenzelm |
Markup.internalK;
|
file |
diff |
annotate
|
| Sun, 29 Jul 2007 14:30:04 +0200 |
wenzelm |
moved Drule.add/del/merge_rules to Thm.add/del/merge_thms;
|
file |
diff |
annotate
|
| Thu, 05 Jul 2007 20:01:36 +0200 |
wenzelm |
added is_reflexive;
|
file |
diff |
annotate
|
| Mon, 25 Jun 2007 00:36:40 +0200 |
wenzelm |
added reasonably efficient add_cterm_frees;
|
file |
diff |
annotate
|
| Thu, 31 May 2007 19:11:19 +0200 |
wenzelm |
made aconvc pervasive;
|
file |
diff |
annotate
|
| Thu, 31 May 2007 18:31:36 +0200 |
wenzelm |
moved aconvc to more_thm.ML;
|
file |
diff |
annotate
|
| Thu, 10 May 2007 00:39:53 +0200 |
wenzelm |
added destructors from drule.ML;
|
file |
diff |
annotate
|
| Sun, 15 Apr 2007 14:31:53 +0200 |
wenzelm |
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
|
file |
diff |
annotate
|
| Sat, 14 Apr 2007 17:36:10 +0200 |
wenzelm |
added read_def_cterms, read_cterm (from thm.ML);
|
file |
diff |
annotate
|
| Wed, 28 Feb 2007 22:05:43 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 26 Feb 2007 23:18:27 +0100 |
wenzelm |
Further operations on type thm, outside the inference kernel.
|
file |
diff |
annotate
|