diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOLCF/Fun2.thy --- a/src/HOLCF/Fun2.thy Sat Dec 01 18:51:46 2001 +0100 +++ b/src/HOLCF/Fun2.thy Sat Dec 01 18:52:32 2001 +0100 @@ -2,15 +2,13 @@ ID: $Id$ Author: Franz Regensburger License: GPL (GNU GENERAL PUBLIC LICENSE) - -Class Instance =>::(term,po)po *) Fun2 = Fun1 + -(* default class is still term !*) +(* default class is still type!*) -instance fun :: (term,po)po (refl_less_fun,antisym_less_fun,trans_less_fun) +instance fun :: (type, po) po (refl_less_fun,antisym_less_fun,trans_less_fun) end