Mon, 08 Nov 2010 15:13:45 -0800 | huffman | implement defl_of_typ using Pattern.rewrite_term instead of DeflData theory data | changeset | files |
Mon, 08 Nov 2010 14:36:17 -0800 | huffman | add function the_sort | changeset | files |
Mon, 08 Nov 2010 14:09:07 -0800 | huffman | refactor tmp_thy code | changeset | files |
Mon, 08 Nov 2010 06:58:09 -0800 | huffman | reorganize Bifinite.thy; simplify some proofs related to bifinite class instances | changeset | files |
Fri, 12 Nov 2010 11:36:01 +0100 | wenzelm | treat pervasive "Interrupt" constructor as illegal -- superseded by Exn.Interrupt for internal use and Exn.is_interrupt/Exn.interrupt in user-space; | changeset | files |
Fri, 12 Nov 2010 10:58:09 +0100 | wenzelm | Laze.force_result: more robust treatment of interrupts stemming from peer group cancellation; | changeset | files |
Thu, 11 Nov 2010 19:58:07 +0100 | wenzelm | more precise treatment of deleted nodes; | changeset | files |
Thu, 11 Nov 2010 18:55:17 +0100 | wenzelm | tuned error message; | changeset | files |