changeset 14854 | 61bdf2ae4dc5 |
parent 14565 | c6dc17aab88a |
child 15377 | 3d99eea28a9b |
--- a/src/FOL/IFOL.thy Tue Jun 01 11:25:26 2004 +0200 +++ b/src/FOL/IFOL.thy Tue Jun 01 12:33:50 2004 +0200 @@ -13,7 +13,7 @@ global -classes "term" < logic +classes "term" defaultsort "term" typedecl o @@ -264,7 +264,7 @@ nonterminals letbinds letbind constdefs - Let :: "['a::logic, 'a => 'b] => ('b::logic)" + Let :: "['a::{}, 'a => 'b] => ('b::{})" "Let(s, f) == f(s)" syntax