| Thu, 05 Jul 2007 00:06:18 +0200 |
wenzelm |
moved mk_cnumeral/mk_cnumber to Tools/numeral.ML;
|
changeset |
files
|
| Thu, 05 Jul 2007 00:06:17 +0200 |
wenzelm |
avoid polymorphic equality;
|
changeset |
files
|
| Thu, 05 Jul 2007 00:06:16 +0200 |
wenzelm |
avoid polymorphic equality;
|
changeset |
files
|
| Thu, 05 Jul 2007 00:06:14 +0200 |
wenzelm |
avoid polymorphic equality;
|
changeset |
files
|
| Thu, 05 Jul 2007 00:06:13 +0200 |
wenzelm |
removed dest_cTrueprop (cf. ObjectLogic.dest_judgment);
|
changeset |
files
|
| Thu, 05 Jul 2007 00:06:12 +0200 |
wenzelm |
Logical operations on numerals (see also HOL/hologic.ML).
|
changeset |
files
|
| Thu, 05 Jul 2007 00:06:11 +0200 |
wenzelm |
added Tools/numeral.ML;
|
changeset |
files
|
| Thu, 05 Jul 2007 00:06:10 +0200 |
wenzelm |
common normalizer_funs, avoid cterm_of;
|
changeset |
files
|
| Thu, 05 Jul 2007 00:06:09 +0200 |
wenzelm |
Numeral.mk_cnumber;
|
changeset |
files
|
| Wed, 04 Jul 2007 21:20:23 +0200 |
aspinall |
PGML abstraction, draft version
|
changeset |
files
|
| Wed, 04 Jul 2007 21:19:34 +0200 |
aspinall |
Use pgml
|
changeset |
files
|
| Wed, 04 Jul 2007 17:21:02 +0200 |
obua |
fixed argument order in calls to Integer.pow
|
changeset |
files
|
| Wed, 04 Jul 2007 16:49:36 +0200 |
wenzelm |
added binop_cong_rule;
|
changeset |
files
|
| Wed, 04 Jul 2007 16:49:35 +0200 |
wenzelm |
export dlo_conv;
|
changeset |
files
|
| Wed, 04 Jul 2007 16:49:34 +0200 |
wenzelm |
replaced HOLogic.Trueprop_conv by ObjectLogic.judgment_conv;
|
changeset |
files
|
| Wed, 04 Jul 2007 14:21:00 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Wed, 04 Jul 2007 14:10:01 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Wed, 04 Jul 2007 13:56:26 +0200 |
paulson |
simplified a proof
|
changeset |
files
|
| Tue, 03 Jul 2007 23:00:42 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 03 Jul 2007 22:27:30 +0200 |
wenzelm |
CONVERSION: handle TYPE | TERM | CTERM | THM;
|
changeset |
files
|
| Tue, 03 Jul 2007 22:27:27 +0200 |
wenzelm |
proper use of ioa_package.ML;
|
changeset |
files
|
| Tue, 03 Jul 2007 22:27:25 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 03 Jul 2007 22:27:19 +0200 |
wenzelm |
tuned is_comb/is_binop -- avoid construction of cterms;
|
changeset |
files
|
| Tue, 03 Jul 2007 22:27:16 +0200 |
wenzelm |
HOLogic.conj_intr/elims;
|
changeset |
files
|
| Tue, 03 Jul 2007 22:27:13 +0200 |
wenzelm |
use mucke_oracle.ML only once;
|
changeset |
files
|
| Tue, 03 Jul 2007 22:27:11 +0200 |
wenzelm |
assume basic HOL context for compilation (antiquotations);
|
changeset |
files
|
| Tue, 03 Jul 2007 22:27:08 +0200 |
wenzelm |
proper use of function_package ML files;
|
changeset |
files
|
| Tue, 03 Jul 2007 22:27:05 +0200 |
wenzelm |
use hologic.ML in basic HOL context;
|
changeset |
files
|