Thu, 05 Jul 2007 20:01:31 +0200 wenzelm renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
Thu, 05 Jul 2007 20:01:30 +0200 wenzelm renamed Conv.is_refl to Thm.is_reflexive;
Thu, 05 Jul 2007 20:01:29 +0200 wenzelm renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
Thu, 05 Jul 2007 20:01:28 +0200 wenzelm simplified ObjectLogic.atomize;
Thu, 05 Jul 2007 20:01:26 +0200 wenzelm renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
Thu, 05 Jul 2007 19:59:01 +0200 aspinall Revert body of pgml to match schema for now [change bad for Broker]
Thu, 05 Jul 2007 19:57:19 +0200 aspinall Classify -- comments as ordinary comments (no undo)
Thu, 05 Jul 2007 00:15:44 +0200 wenzelm tuned;
Thu, 05 Jul 2007 00:06:25 +0200 wenzelm avoid polymorphic equality;
Thu, 05 Jul 2007 00:06:24 +0200 wenzelm sort_le: tuned eq case;
Thu, 05 Jul 2007 00:06:23 +0200 wenzelm tuned goal conversion interfaces;
Thu, 05 Jul 2007 00:06:22 +0200 wenzelm else_conv: only handle THM | CTERM | TERM | TYPE;
Thu, 05 Jul 2007 00:06:20 +0200 wenzelm avoid polymorphic equality;
Thu, 05 Jul 2007 00:06:19 +0200 wenzelm tuned;
Thu, 05 Jul 2007 00:06:18 +0200 wenzelm moved mk_cnumeral/mk_cnumber to Tools/numeral.ML;
Thu, 05 Jul 2007 00:06:17 +0200 wenzelm avoid polymorphic equality;
Thu, 05 Jul 2007 00:06:16 +0200 wenzelm avoid polymorphic equality;
Thu, 05 Jul 2007 00:06:14 +0200 wenzelm avoid polymorphic equality;
Thu, 05 Jul 2007 00:06:13 +0200 wenzelm removed dest_cTrueprop (cf. ObjectLogic.dest_judgment);
Thu, 05 Jul 2007 00:06:12 +0200 wenzelm Logical operations on numerals (see also HOL/hologic.ML).
Thu, 05 Jul 2007 00:06:11 +0200 wenzelm added Tools/numeral.ML;
Thu, 05 Jul 2007 00:06:10 +0200 wenzelm common normalizer_funs, avoid cterm_of;
Thu, 05 Jul 2007 00:06:09 +0200 wenzelm Numeral.mk_cnumber;
Wed, 04 Jul 2007 21:20:23 +0200 aspinall PGML abstraction, draft version
Wed, 04 Jul 2007 21:19:34 +0200 aspinall Use pgml
Wed, 04 Jul 2007 17:21:02 +0200 obua fixed argument order in calls to Integer.pow
Wed, 04 Jul 2007 16:49:36 +0200 wenzelm added binop_cong_rule;
Wed, 04 Jul 2007 16:49:35 +0200 wenzelm export dlo_conv;
Wed, 04 Jul 2007 16:49:34 +0200 wenzelm replaced HOLogic.Trueprop_conv by ObjectLogic.judgment_conv;
Wed, 04 Jul 2007 14:21:00 +0200 nipkow *** empty log message ***
Wed, 04 Jul 2007 14:10:01 +0200 nipkow *** empty log message ***
Wed, 04 Jul 2007 13:56:26 +0200 paulson simplified a proof
Tue, 03 Jul 2007 23:00:42 +0200 wenzelm tuned;
Tue, 03 Jul 2007 22:27:30 +0200 wenzelm CONVERSION: handle TYPE | TERM | CTERM | THM;
Tue, 03 Jul 2007 22:27:27 +0200 wenzelm proper use of ioa_package.ML;
Tue, 03 Jul 2007 22:27:25 +0200 wenzelm tuned;
Tue, 03 Jul 2007 22:27:19 +0200 wenzelm tuned is_comb/is_binop -- avoid construction of cterms;
Tue, 03 Jul 2007 22:27:16 +0200 wenzelm HOLogic.conj_intr/elims;
Tue, 03 Jul 2007 22:27:13 +0200 wenzelm use mucke_oracle.ML only once;
Tue, 03 Jul 2007 22:27:11 +0200 wenzelm assume basic HOL context for compilation (antiquotations);
Tue, 03 Jul 2007 22:27:08 +0200 wenzelm proper use of function_package ML files;
Tue, 03 Jul 2007 22:27:05 +0200 wenzelm use hologic.ML in basic HOL context;
Tue, 03 Jul 2007 21:56:25 +0200 paulson to handle non-atomic assumptions
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);
Tue, 03 Jul 2007 18:42:09 +0200 huffman convert instance proofs to Isar style
Tue, 03 Jul 2007 18:00:57 +0200 chaieb Dependency on reflection_data.ML to build HOL-ex
Tue, 03 Jul 2007 17:50:00 +0200 chaieb Generalized case for atoms. Selection of environment lists is allowed more than once.
Tue, 03 Jul 2007 17:49:58 +0200 chaieb More examples
Tue, 03 Jul 2007 17:49:55 +0200 chaieb reflection and reification methods now manage Context data
Tue, 03 Jul 2007 17:49:53 +0200 chaieb Context Data for the reflection and reification methods
Tue, 03 Jul 2007 17:28:36 +0200 huffman rename class dom to ring_1_no_zero_divisors
Tue, 03 Jul 2007 17:17:17 +0200 wenzelm rewrite_goal_tac;
Tue, 03 Jul 2007 17:17:16 +0200 wenzelm replaced Conv.goals_conv by Conv.prems_conv;
Tue, 03 Jul 2007 17:17:15 +0200 wenzelm exported meta_rewrite_conv;
Tue, 03 Jul 2007 17:17:15 +0200 wenzelm CONVERSION tactical;
Tue, 03 Jul 2007 17:17:13 +0200 wenzelm removed obsolete eta_long_tac;
Tue, 03 Jul 2007 17:17:13 +0200 wenzelm added CONVERSION tactical;
Tue, 03 Jul 2007 17:17:11 +0200 wenzelm tuned rotate_prems;
Tue, 03 Jul 2007 17:17:11 +0200 wenzelm moved (asm_)rewrite_goal_tac from goal.ML to meta_simplifier.ML (no longer depends on SELECT_GOAL);
Tue, 03 Jul 2007 17:17:09 +0200 wenzelm removed obsolete mk_conjunction_list, intr/elim_list;
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip