| Tue, 03 Jul 2007 17:17:13 +0200 |
wenzelm |
added CONVERSION tactical;
|
changeset |
files
|
| Tue, 03 Jul 2007 17:17:11 +0200 |
wenzelm |
tuned rotate_prems;
|
changeset |
files
|
| 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);
|
changeset |
files
|
| Tue, 03 Jul 2007 17:17:09 +0200 |
wenzelm |
removed obsolete mk_conjunction_list, intr/elim_list;
|
changeset |
files
|
| Tue, 03 Jul 2007 17:17:09 +0200 |
wenzelm |
removed obsolete goals_conv (cf. prems_conv);
|
changeset |
files
|
| Tue, 03 Jul 2007 17:17:07 +0200 |
wenzelm |
Conjunction.intr/elim_balanced;
|
changeset |
files
|
| Tue, 03 Jul 2007 17:17:07 +0200 |
wenzelm |
CONVERSION tactical;
|
changeset |
files
|
| Tue, 03 Jul 2007 17:17:06 +0200 |
wenzelm |
Conjunction.mk_conjunction_balanced;
|
changeset |
files
|
| Tue, 03 Jul 2007 17:17:04 +0200 |
wenzelm |
CONVERSION tactical;
|
changeset |
files
|
| Tue, 03 Jul 2007 15:23:11 +0200 |
nipkow |
Fixed problem with patterns in lambdas
|
changeset |
files
|
| Tue, 03 Jul 2007 14:48:27 +0200 |
krauss |
fixed an issue with mutual recursion
|
changeset |
files
|
| Tue, 03 Jul 2007 01:26:06 +0200 |
huffman |
instance pordered_comm_ring < pordered_ring
|
changeset |
files
|
| Mon, 02 Jul 2007 23:14:06 +0200 |
nipkow |
Added pattern maatching for lambda abstraction
|
changeset |
files
|
| Mon, 02 Jul 2007 16:42:37 +0200 |
paulson |
revised the discussion of type classes
|
changeset |
files
|