changeset 1410 | 324aa8134639 |
parent 1274 | ea0668a1c0ba |
child 1461 | 6bcb44e4d6e5 |
--- a/src/HOLCF/explicit_domains/Dnat.ML Mon Dec 18 13:09:17 1995 +0100 +++ b/src/HOLCF/explicit_domains/Dnat.ML Wed Dec 20 16:28:51 1995 +0100 @@ -499,7 +499,7 @@ ]); -qed_goalw "dnat_flat" Dnat.thy [flat_def] "flat(dzero)" +qed_goalw "dnat_flat" Dnat.thy [is_flat_def] "is_flat(dzero)" (fn prems => [ (rtac allI 1),