| 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
|
| Tue, 03 Jul 2007 21:56:25 +0200 |
paulson |
to handle non-atomic assumptions
|
changeset |
files
|
| Tue, 03 Jul 2007 20:26:08 +0200 |
wenzelm |
rename class dom to ring_1_no_zero_divisors (cf. HOL/Ring_and_Field.thy 1.84 by huffman);
|
changeset |
files
|
| Tue, 03 Jul 2007 18:42:09 +0200 |
huffman |
convert instance proofs to Isar style
|
changeset |
files
|
| Tue, 03 Jul 2007 18:00:57 +0200 |
chaieb |
Dependency on reflection_data.ML to build HOL-ex
|
changeset |
files
|
| Tue, 03 Jul 2007 17:50:00 +0200 |
chaieb |
Generalized case for atoms. Selection of environment lists is allowed more than once.
|
changeset |
files
|
| Tue, 03 Jul 2007 17:49:58 +0200 |
chaieb |
More examples
|
changeset |
files
|
| Tue, 03 Jul 2007 17:49:55 +0200 |
chaieb |
reflection and reification methods now manage Context data
|
changeset |
files
|
| Tue, 03 Jul 2007 17:49:53 +0200 |
chaieb |
Context Data for the reflection and reification methods
|
changeset |
files
|
| Tue, 03 Jul 2007 17:28:36 +0200 |
huffman |
rename class dom to ring_1_no_zero_divisors
|
changeset |
files
|
| Tue, 03 Jul 2007 17:17:17 +0200 |
wenzelm |
rewrite_goal_tac;
|
changeset |
files
|
| Tue, 03 Jul 2007 17:17:16 +0200 |
wenzelm |
replaced Conv.goals_conv by Conv.prems_conv;
|
changeset |
files
|
| Tue, 03 Jul 2007 17:17:15 +0200 |
wenzelm |
exported meta_rewrite_conv;
|
changeset |
files
|
| Tue, 03 Jul 2007 17:17:15 +0200 |
wenzelm |
CONVERSION tactical;
|
changeset |
files
|