changeset 41229 | d797baa3d57c |
parent 39557 | fe5722fce758 |
child 41310 | 65631ca437c9 |
41228:e1fce873b814 | 41229:d797baa3d57c |
---|---|
752 mp |
752 mp |
753 trans |
753 trans |
754 |
754 |
755 subsection {* ``Let'' declarations *} |
755 subsection {* ``Let'' declarations *} |
756 |
756 |
757 nonterminals letbinds letbind |
757 nonterminal letbinds and letbind |
758 |
758 |
759 definition Let :: "['a::{}, 'a => 'b] => ('b::{})" where |
759 definition Let :: "['a::{}, 'a => 'b] => ('b::{})" where |
760 "Let(s, f) == f(s)" |
760 "Let(s, f) == f(s)" |
761 |
761 |
762 syntax |
762 syntax |