| 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
|
| Mon, 02 Jul 2007 10:43:20 +0200 |
chaieb |
Generic QE need no Context anymore
|
changeset |
files
|
| Mon, 02 Jul 2007 10:43:19 +0200 |
chaieb |
Handle exception TYPE
|
changeset |
files
|
| Mon, 02 Jul 2007 10:43:17 +0200 |
chaieb |
Tuned proofs
|
changeset |
files
|
| Sat, 30 Jun 2007 17:30:10 +0200 |
obua |
added ordered_ring and ordered_semiring
|
changeset |
files
|