wenzelm [Tue, 03 Jul 2007 17:17:13 +0200] rev 23539
removed obsolete eta_long_tac;
wenzelm [Tue, 03 Jul 2007 17:17:13 +0200] rev 23538
added CONVERSION tactical;
tuned signature;
wenzelm [Tue, 03 Jul 2007 17:17:11 +0200] rev 23537
tuned rotate_prems;
tuned comments;
wenzelm [Tue, 03 Jul 2007 17:17:11 +0200] rev 23536
moved (asm_)rewrite_goal_tac from goal.ML to meta_simplifier.ML (no longer depends on SELECT_GOAL);
wenzelm [Tue, 03 Jul 2007 17:17:09 +0200] rev 23535
removed obsolete mk_conjunction_list, intr/elim_list;
wenzelm [Tue, 03 Jul 2007 17:17:09 +0200] rev 23534
removed obsolete goals_conv (cf. prems_conv);
added efficient goal_conv_rule;
tuned comments;
wenzelm [Tue, 03 Jul 2007 17:17:07 +0200] rev 23533
Conjunction.intr/elim_balanced;
CONVERSION tactical;
tuned;
wenzelm [Tue, 03 Jul 2007 17:17:07 +0200] rev 23532
CONVERSION tactical;
Simplifier.rewrite_goal_tac;
wenzelm [Tue, 03 Jul 2007 17:17:06 +0200] rev 23531
Conjunction.mk_conjunction_balanced;
wenzelm [Tue, 03 Jul 2007 17:17:04 +0200] rev 23530
CONVERSION tactical;
nipkow [Tue, 03 Jul 2007 15:23:11 +0200] rev 23529
Fixed problem with patterns in lambdas
krauss [Tue, 03 Jul 2007 14:48:27 +0200] rev 23528
fixed an issue with mutual recursion
huffman [Tue, 03 Jul 2007 01:26:06 +0200] rev 23527
instance pordered_comm_ring < pordered_ring
nipkow [Mon, 02 Jul 2007 23:14:06 +0200] rev 23526
Added pattern maatching for lambda abstraction
paulson [Mon, 02 Jul 2007 16:42:37 +0200] rev 23525
revised the discussion of type classes
chaieb [Mon, 02 Jul 2007 10:43:20 +0200] rev 23524
Generic QE need no Context anymore
chaieb [Mon, 02 Jul 2007 10:43:19 +0200] rev 23523
Handle exception TYPE
chaieb [Mon, 02 Jul 2007 10:43:17 +0200] rev 23522
Tuned proofs
obua [Sat, 30 Jun 2007 17:30:10 +0200] rev 23521
added ordered_ring and ordered_semiring
haftmann [Fri, 29 Jun 2007 21:23:05 +0200] rev 23520
tuned arithmetic modules
paulson [Fri, 29 Jun 2007 18:21:25 +0200] rev 23519
bug fixes to proof reconstruction
haftmann [Fri, 29 Jun 2007 16:05:00 +0200] rev 23518
dropped local cg cmd
haftmann [Thu, 28 Jun 2007 19:09:43 +0200] rev 23517
dropped toplevel lcm, gcd
haftmann [Thu, 28 Jun 2007 19:09:41 +0200] rev 23516
proper collapse_let
haftmann [Thu, 28 Jun 2007 19:09:38 +0200] rev 23515
new code generator framework
haftmann [Thu, 28 Jun 2007 19:09:36 +0200] rev 23514
dropped Library.lcm
haftmann [Thu, 28 Jun 2007 19:09:35 +0200] rev 23513
tuned
haftmann [Thu, 28 Jun 2007 19:09:34 +0200] rev 23512
code generation for dvd
haftmann [Thu, 28 Jun 2007 19:09:32 +0200] rev 23511
simplified keyword setup
paulson [Wed, 27 Jun 2007 12:41:36 +0200] rev 23510
GPL -> BSD