diff -r 2e9a86203d59 -r 934a58983311 Univ.thy --- a/Univ.thy Thu Mar 17 14:08:08 1994 +0100 +++ b/Univ.thy Thu Mar 17 17:02:49 1994 +0100 @@ -12,8 +12,13 @@ *) Univ = Arith + -types node 1 -arities node :: (term)term + +types + 'a node + +arities + node :: (term)term + consts Least :: "(nat=>bool) => nat" (binder "LEAST " 10)