author | wenzelm |
Mon, 04 Sep 2000 21:20:14 +0200 | |
changeset 9833 | 193dc80eaee9 |
parent 9832 | 2092298f7421 |
child 9834 | 109b11c4e77e |
--- a/src/HOL/WF_Rel.thy Mon Sep 04 21:19:27 2000 +0200 +++ b/src/HOL/WF_Rel.thy Mon Sep 04 21:20:14 2000 +0200 @@ -12,7 +12,7 @@ WF_Rel = Finite + -(* actually belongs to Finite.thy *) +(* actually belongs to theory Finite *) instance unit :: finite (finite_unit) instance "*" :: (finite,finite) finite (finite_Prod)