isabelle: src/ZF/Let.ML@2a705d1af4dc (annotated)

1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1450 diff changeset	1	(* Title: ZF/Let
1061 8897213195c0 Definition of 'let' declarations, from HOL lcp parents: diff changeset	2	ID: $Id$
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1450 diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
1061 8897213195c0 Definition of 'let' declarations, from HOL lcp parents: diff changeset	4	Copyright 1995 University of Cambridge
8897213195c0 Definition of 'let' declarations, from HOL lcp parents: diff changeset	5
8897213195c0 Definition of 'let' declarations, from HOL lcp parents: diff changeset	6	Let expressions -- borrowed from HOL
8897213195c0 Definition of 'let' declarations, from HOL lcp parents: diff changeset	7	*)
8897213195c0 Definition of 'let' declarations, from HOL lcp parents: diff changeset	8
9907 473a6604da94 tuned ML code (the_context, bind_thms(s)); wenzelm parents: 1461 diff changeset	9	val [prem] = goalw (the_context ())
1061 8897213195c0 Definition of 'let' declarations, from HOL lcp parents: diff changeset	10	[Let_def] "(!!x. x=t ==> P(u(x))) ==> P(let x=t in u(x))";
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1450 diff changeset	11	by (rtac (refl RS prem) 1);
1450 19a256c8086d Renamed letI to LetI (for consistency) paulson parents: 1061 diff changeset	12	qed "LetI";