changeset 41229 | d797baa3d57c |
parent 39557 | fe5722fce758 |
child 41310 | 65631ca437c9 |
--- a/src/FOL/IFOL.thy Fri Dec 17 17:08:56 2010 +0100 +++ b/src/FOL/IFOL.thy Fri Dec 17 17:43:54 2010 +0100 @@ -754,7 +754,7 @@ subsection {* ``Let'' declarations *} -nonterminals letbinds letbind +nonterminal letbinds and letbind definition Let :: "['a::{}, 'a => 'b] => ('b::{})" where "Let(s, f) == f(s)"