Wed, 12 Aug 1998 16:23:25 +0200 | oheimb | cleanup for Fun.thy: | changeset | files |
Wed, 12 Aug 1998 16:21:18 +0200 | oheimb | the splitter is now defined as a functor | changeset | files |
Wed, 12 Aug 1998 16:20:49 +0200 | oheimb | renamed mk_meta_eq to meta_eq | changeset | files |
Wed, 12 Aug 1998 16:16:49 +0200 | oheimb | removed superfluous o_apply | changeset | files |
Wed, 12 Aug 1998 16:15:37 +0200 | oheimb | streamlined proofs with new hoare_conseq1, hoare_conseq2 | changeset | files |
Wed, 12 Aug 1998 16:04:27 +0200 | oheimb | defined map_upd by translation via fun_upd | changeset | files |