| Fri, 03 Jun 2005 23:13:08 +0200 | huffman | renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs. | changeset | files |
| Fri, 03 Jun 2005 22:21:43 +0200 | huffman | added theorem ch2ch_lub | changeset | files |
| Fri, 03 Jun 2005 22:07:30 +0200 | huffman | renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict | changeset | files |
| Fri, 03 Jun 2005 22:04:17 +0200 | huffman | added theorems diag_lub and ex_lub | changeset | files |
| Fri, 03 Jun 2005 14:35:33 +0200 | webertj | fixed a typo in the gfp interpreter | changeset | files |
| Fri, 03 Jun 2005 12:41:28 +0200 | paulson | no longer emits literals for type class HOL.type; also minor tidying | changeset | files |
| Fri, 03 Jun 2005 01:08:07 +0200 | obua | Integrates cycle detection in definitions with finalconsts | changeset | files |