added Induct/Binary_Trees.thy, Induct/Tree_Forest (converted from
former ex/TF.ML ex/TF.thy ex/Term.ML ex/Term.thy);
(* Title: ZF/Let
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1995 University of Cambridge
Let expressions, and tuple pattern-matching (borrowed from HOL)
*)
Let = FOL +
types
letbinds letbind
consts
Let :: ['a::logic, 'a => 'b] => ('b::logic)
syntax
"_bind" :: [pttrn, 'a] => letbind ("(2_ =/ _)" 10)
"" :: letbind => letbinds ("_")
"_binds" :: [letbind, letbinds] => letbinds ("_;/ _")
"_Let" :: [letbinds, 'a] => 'a ("(let (_)/ in (_))" 10)
translations
"_Let(_binds(b, bs), e)" == "_Let(b, _Let(bs, e))"
"let x = a in e" == "Let(a, %x. e)"
defs
Let_def "Let(s, f) == f(s)"
end