equal
deleted
inserted
replaced
758 |
758 |
759 subsection {* ``Let'' declarations *} |
759 subsection {* ``Let'' declarations *} |
760 |
760 |
761 nonterminals letbinds letbind |
761 nonterminals letbinds letbind |
762 |
762 |
763 constdefs |
763 definition Let :: "['a::{}, 'a => 'b] => ('b::{})" where |
764 Let :: "['a::{}, 'a => 'b] => ('b::{})" |
|
765 "Let(s, f) == f(s)" |
764 "Let(s, f) == f(s)" |
766 |
765 |
767 syntax |
766 syntax |
768 "_bind" :: "[pttrn, 'a] => letbind" ("(2_ =/ _)" 10) |
767 "_bind" :: "[pttrn, 'a] => letbind" ("(2_ =/ _)" 10) |
769 "" :: "letbind => letbinds" ("_") |
768 "" :: "letbind => letbinds" ("_") |