isabelle: src/ZF/Let.ML@b890c27c93d6 (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
8897213195c0 Definition of 'let' declarations, from HOL lcp parents: diff changeset	9	open Let;
8897213195c0 Definition of 'let' declarations, from HOL lcp parents: diff changeset	10
8897213195c0 Definition of 'let' declarations, from HOL lcp parents: diff changeset	11	val [prem] = goalw thy
8897213195c0 Definition of 'let' declarations, from HOL lcp parents: diff changeset	12	[Let_def] "(!!x. x=t ==> P(u(x))) ==> P(let x=t in u(x))";
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1450 diff changeset	13	by (rtac (refl RS prem) 1);
1450 19a256c8086d Renamed letI to LetI (for consistency) paulson parents: 1061 diff changeset	14	qed "LetI";

author	wenzelm
	Thu, 27 Aug 1998 18:34:55 +0200
changeset 5395	b890c27c93d6
parent 1461	6bcb44e4d6e5
child 9907	473a6604da94
permissions	-rw-r--r--