diff -r 340d21c86440 -r 5d95fe89f501 HOL.thy --- a/HOL.thy Mon Dec 13 18:43:03 1993 +0100 +++ b/HOL.thy Tue Dec 14 18:05:22 1993 +0100 @@ -19,6 +19,7 @@ types bool 0 + letbinds, letbind 0 arities fun :: (term, term) term @@ -43,7 +44,10 @@ Ex1 :: "('a => bool) => bool" (binder "?! " 10) Let :: "['a, 'a => 'b] => 'b" - "@Let" :: "[idt, 'a, 'b] => 'b" ("(let _ = (2_)/ in (2_))" 10) + "_bind" :: "[idt, 'a] => letbind" ("(2_ =/ _)" 10) + "" :: "letbind => letbinds" ("_") + "_binds" :: "[letbind, letbinds] => letbinds" ("_;/ _") + "_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" 10) (* Alternative Quantifiers *) @@ -72,8 +76,8 @@ "EX xs. P" => "? xs. P" "EX! xs. P" => "?! xs. P" "x ~= y" == "~ (x = y)" - "let x = s in t" == "Let(s, %x. t)" - + "_Let(_binds(b, bs), e)" == "_Let(b, _Let(bs, e))" + "let x = a in e" == "Let(a, %x. e)" rules