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;
Tue, 03 Jul 2007 17:17:09 +0200 wenzelm removed obsolete goals_conv (cf. prems_conv);
Tue, 03 Jul 2007 17:17:07 +0200 wenzelm Conjunction.intr/elim_balanced;
Tue, 03 Jul 2007 17:17:07 +0200 wenzelm CONVERSION tactical;
Tue, 03 Jul 2007 17:17:06 +0200 wenzelm Conjunction.mk_conjunction_balanced;
Tue, 03 Jul 2007 17:17:04 +0200 wenzelm CONVERSION tactical;
Tue, 03 Jul 2007 15:23:11 +0200 nipkow Fixed problem with patterns in lambdas
Tue, 03 Jul 2007 14:48:27 +0200 krauss fixed an issue with mutual recursion
Tue, 03 Jul 2007 01:26:06 +0200 huffman instance pordered_comm_ring < pordered_ring
Mon, 02 Jul 2007 23:14:06 +0200 nipkow Added pattern maatching for lambda abstraction
Mon, 02 Jul 2007 16:42:37 +0200 paulson revised the discussion of type classes
Mon, 02 Jul 2007 10:43:20 +0200 chaieb Generic QE need no Context anymore
Mon, 02 Jul 2007 10:43:19 +0200 chaieb Handle exception TYPE
Mon, 02 Jul 2007 10:43:17 +0200 chaieb Tuned proofs
Sat, 30 Jun 2007 17:30:10 +0200 obua added ordered_ring and ordered_semiring
Fri, 29 Jun 2007 21:23:05 +0200 haftmann tuned arithmetic modules
Fri, 29 Jun 2007 18:21:25 +0200 paulson bug fixes to proof reconstruction
Fri, 29 Jun 2007 16:05:00 +0200 haftmann dropped local cg cmd
Thu, 28 Jun 2007 19:09:43 +0200 haftmann dropped toplevel lcm, gcd
Thu, 28 Jun 2007 19:09:41 +0200 haftmann proper collapse_let
Thu, 28 Jun 2007 19:09:38 +0200 haftmann new code generator framework
Thu, 28 Jun 2007 19:09:36 +0200 haftmann dropped Library.lcm
Thu, 28 Jun 2007 19:09:35 +0200 haftmann tuned
Thu, 28 Jun 2007 19:09:34 +0200 haftmann code generation for dvd
Thu, 28 Jun 2007 19:09:32 +0200 haftmann simplified keyword setup
Wed, 27 Jun 2007 12:41:36 +0200 paulson GPL -> BSD
Wed, 27 Jun 2007 11:06:43 +0200 nipkow *** empty log message ***
Tue, 26 Jun 2007 18:32:53 +0200 paulson updated for metis method
Tue, 26 Jun 2007 18:32:24 +0200 paulson recoded
Tue, 26 Jun 2007 18:28:40 +0200 paulson simplified
Tue, 26 Jun 2007 15:48:24 +0200 paulson completed some references
Tue, 26 Jun 2007 15:48:09 +0200 paulson changes for type class ring_no_zero_divisors
Tue, 26 Jun 2007 13:02:28 +0200 nipkow *** empty log message ***
Tue, 26 Jun 2007 13:01:48 +0200 nipkow added NBE
Tue, 26 Jun 2007 08:42:04 +0200 nipkow removed removed lemmas
Tue, 26 Jun 2007 00:35:14 +0200 wenzelm fixed undo: try undos_proof first!
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip