| 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
|