src/ZF/Let.ML
changeset 1461 6bcb44e4d6e5
parent 1450 19a256c8086d
child 9907 473a6604da94
--- a/src/ZF/Let.ML	Mon Jan 29 14:16:13 1996 +0100
+++ b/src/ZF/Let.ML	Tue Jan 30 13:42:57 1996 +0100
@@ -1,6 +1,6 @@
-(*  Title: 	ZF/Let
+(*  Title:      ZF/Let
     ID:         $Id$
-    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1995  University of Cambridge
 
 Let expressions -- borrowed from HOL
@@ -10,5 +10,5 @@
 
 val [prem] = goalw thy
     [Let_def] "(!!x. x=t ==> P(u(x))) ==> P(let x=t in u(x))";
-br (refl RS prem) 1;
+by (rtac (refl RS prem) 1);
 qed "LetI";