Mercurial Mercurial > repos > isabelle / changelog
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
(0) -10000 -3000 -1000 -300 -100 -50 -28 +28 +50 +100 +300 +1000 +3000 +10000 +30000 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Wed, 04 Jul 2007 14:21:00 +0200 *** empty log message ***
changeset
nipkow [Wed, 04 Jul 2007 14:21:00 +0200] rev 23565
*** empty log message ***
Wed, 04 Jul 2007 14:10:01 +0200 *** empty log message ***
changeset
nipkow [Wed, 04 Jul 2007 14:10:01 +0200] rev 23564
*** empty log message ***
Wed, 04 Jul 2007 13:56:26 +0200 simplified a proof
changeset
paulson [Wed, 04 Jul 2007 13:56:26 +0200] rev 23563
simplified a proof
Tue, 03 Jul 2007 23:00:42 +0200 tuned;
changeset
wenzelm [Tue, 03 Jul 2007 23:00:42 +0200] rev 23562
tuned;
Tue, 03 Jul 2007 22:27:30 +0200 CONVERSION: handle TYPE | TERM | CTERM | THM;
changeset
wenzelm [Tue, 03 Jul 2007 22:27:30 +0200] rev 23561
CONVERSION: handle TYPE | TERM | CTERM | THM;
Tue, 03 Jul 2007 22:27:27 +0200 proper use of ioa_package.ML;
changeset
wenzelm [Tue, 03 Jul 2007 22:27:27 +0200] rev 23560
proper use of ioa_package.ML;
Tue, 03 Jul 2007 22:27:25 +0200 tuned;
changeset
wenzelm [Tue, 03 Jul 2007 22:27:25 +0200] rev 23559
tuned;
Tue, 03 Jul 2007 22:27:19 +0200 tuned is_comb/is_binop -- avoid construction of cterms;
changeset
wenzelm [Tue, 03 Jul 2007 22:27:19 +0200] rev 23558
tuned is_comb/is_binop -- avoid construction of cterms; removed conjunction rules (cf. HOLogic.conj_XXX);
Tue, 03 Jul 2007 22:27:16 +0200 HOLogic.conj_intr/elims;
changeset
wenzelm [Tue, 03 Jul 2007 22:27:16 +0200] rev 23557
HOLogic.conj_intr/elims; removed obsolete assocd/assoc; removed dead string_of_pol; tuned;
Tue, 03 Jul 2007 22:27:13 +0200 use mucke_oracle.ML only once;
changeset
wenzelm [Tue, 03 Jul 2007 22:27:13 +0200] rev 23556
use mucke_oracle.ML only once;
Tue, 03 Jul 2007 22:27:11 +0200 assume basic HOL context for compilation (antiquotations);
changeset
wenzelm [Tue, 03 Jul 2007 22:27:11 +0200] rev 23555
assume basic HOL context for compilation (antiquotations); added dest_cTrueprop; tuned Trueprop_conv; added low-level conj_intr/elim/elis (dire need for @{rule} antiquotation!);
Tue, 03 Jul 2007 22:27:08 +0200 proper use of function_package ML files;
changeset
wenzelm [Tue, 03 Jul 2007 22:27:08 +0200] rev 23554
proper use of function_package ML files;
Tue, 03 Jul 2007 22:27:05 +0200 use hologic.ML in basic HOL context;
changeset
wenzelm [Tue, 03 Jul 2007 22:27:05 +0200] rev 23553
use hologic.ML in basic HOL context; tuned proofs;
Tue, 03 Jul 2007 21:56:25 +0200 to handle non-atomic assumptions
changeset
paulson [Tue, 03 Jul 2007 21:56:25 +0200] rev 23552
to handle non-atomic assumptions
Tue, 03 Jul 2007 20:26:08 +0200 rename class dom to ring_1_no_zero_divisors (cf. HOL/Ring_and_Field.thy 1.84 by huffman);
changeset
wenzelm [Tue, 03 Jul 2007 20:26:08 +0200] rev 23551
rename class dom to ring_1_no_zero_divisors (cf. HOL/Ring_and_Field.thy 1.84 by huffman);
Tue, 03 Jul 2007 18:42:09 +0200 convert instance proofs to Isar style
changeset
huffman [Tue, 03 Jul 2007 18:42:09 +0200] rev 23550
convert instance proofs to Isar style
Tue, 03 Jul 2007 18:00:57 +0200 Dependency on reflection_data.ML to build HOL-ex
changeset
chaieb [Tue, 03 Jul 2007 18:00:57 +0200] rev 23549
Dependency on reflection_data.ML to build HOL-ex
Tue, 03 Jul 2007 17:50:00 +0200 Generalized case for atoms. Selection of environment lists is allowed more than once.
changeset
chaieb [Tue, 03 Jul 2007 17:50:00 +0200] rev 23548
Generalized case for atoms. Selection of environment lists is allowed more than once.
Tue, 03 Jul 2007 17:49:58 +0200 More examples
changeset
chaieb [Tue, 03 Jul 2007 17:49:58 +0200] rev 23547
More examples
Tue, 03 Jul 2007 17:49:55 +0200 reflection and reification methods now manage Context data
changeset
chaieb [Tue, 03 Jul 2007 17:49:55 +0200] rev 23546
reflection and reification methods now manage Context data
Tue, 03 Jul 2007 17:49:53 +0200 Context Data for the reflection and reification methods
changeset
chaieb [Tue, 03 Jul 2007 17:49:53 +0200] rev 23545
Context Data for the reflection and reification methods
Tue, 03 Jul 2007 17:28:36 +0200 rename class dom to ring_1_no_zero_divisors
changeset
huffman [Tue, 03 Jul 2007 17:28:36 +0200] rev 23544
rename class dom to ring_1_no_zero_divisors
Tue, 03 Jul 2007 17:17:17 +0200 rewrite_goal_tac;
changeset
wenzelm [Tue, 03 Jul 2007 17:17:17 +0200] rev 23543
rewrite_goal_tac;
Tue, 03 Jul 2007 17:17:16 +0200 replaced Conv.goals_conv by Conv.prems_conv;
changeset
wenzelm [Tue, 03 Jul 2007 17:17:16 +0200] rev 23542
replaced Conv.goals_conv by Conv.prems_conv;
Tue, 03 Jul 2007 17:17:15 +0200 exported meta_rewrite_conv;
changeset
wenzelm [Tue, 03 Jul 2007 17:17:15 +0200] rev 23541
exported meta_rewrite_conv; CONVERSION tactical;
Tue, 03 Jul 2007 17:17:15 +0200 CONVERSION tactical;
changeset
wenzelm [Tue, 03 Jul 2007 17:17:15 +0200] rev 23540
CONVERSION tactical; MetaSimplifier.rewrite_goal_tac;
Tue, 03 Jul 2007 17:17:13 +0200 removed obsolete eta_long_tac;
changeset
wenzelm [Tue, 03 Jul 2007 17:17:13 +0200] rev 23539
removed obsolete eta_long_tac;
Tue, 03 Jul 2007 17:17:13 +0200 added CONVERSION tactical;
changeset
wenzelm [Tue, 03 Jul 2007 17:17:13 +0200] rev 23538
added CONVERSION tactical; tuned signature;
(0) -10000 -3000 -1000 -300 -100 -50 -28 +28 +50 +100 +300 +1000 +3000 +10000 +30000 tip
isabelle