# HG changeset patch # User lcp # Date 797853795 -7200 # Node ID 8897213195c07fe03c6257ec65441b9923d221f4 # Parent a122584b5cc56d75cf89cb29c2215cadd83e03e8 Definition of 'let' declarations, from HOL diff -r a122584b5cc5 -r 8897213195c0 src/ZF/Let.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Let.ML Fri Apr 14 12:03:15 1995 +0200 @@ -0,0 +1,14 @@ +(* Title: ZF/Let + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1995 University of Cambridge + +Let expressions -- borrowed from HOL +*) + +open Let; + +val [prem] = goalw thy + [Let_def] "(!!x. x=t ==> P(u(x))) ==> P(let x=t in u(x))"; +br (refl RS prem) 1; +qed "letI"; diff -r a122584b5cc5 -r 8897213195c0 src/ZF/Let.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Let.thy Fri Apr 14 12:03:15 1995 +0200 @@ -0,0 +1,30 @@ +(* Title: ZF/Let + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1995 University of Cambridge + +Let expressions -- borrowed from HOL +*) + +Let = ZF + + +types + letbinds letbind + +consts + Let :: "['a, 'a => 'b] => 'b" + +syntax + "_bind" :: "[idt, '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