# HG changeset patch
# User wenzelm
# Date 947170818 -3600
# Node ID aca11f954993a82566f478a33f438a3025f60d2c
# Parent  ce4bb031d664b068a580b992a0b862592a0e4400
obtain: renamed 'in' to 'where';

diff -r ce4bb031d664 -r aca11f954993 src/HOL/Isar_examples/W_correct.thy
--- a/src/HOL/Isar_examples/W_correct.thy	Wed Jan 05 20:49:37 2000 +0100
+++ b/src/HOL/Isar_examples/W_correct.thy	Thu Jan 06 16:00:18 2000 +0100
@@ -113,7 +113,7 @@
       fix a s t m n;
       assume "Ok (s, t, m) = W (Abs e) a n";
       thus "$ s a |- Abs e :: t";
-	obtain t' in "t = s n -> t'" "Ok (s, t', m) = W e (TVar n # a) (Suc n)";
+	obtain t' where "t = s n -> t'" "Ok (s, t', m) = W e (TVar n # a) (Suc n)";
 	  by (rule rev_mp) simp;
 	with hyp; show ?thesis; by (force intro: has_type.AbsI);
       qed;
@@ -124,7 +124,7 @@
     proof (intro allI impI);
       fix a s t m n; assume "Ok (s, t, m) = W (App e1 e2) a n";
       thus "$ s a |- App e1 e2 :: t";
-	obtain s1 t1 n1 s2 t2 n2 u in
+	obtain s1 t1 n1 s2 t2 n2 u where
           s: "s = $ u o $ s2 o s1"
           and t: "t = u n2"
           and mgu_ok: "mgu ($ s2 t1) (t2 -> TVar n2) = Ok u"
diff -r ce4bb031d664 -r aca11f954993 src/HOL/Real/HahnBanach/HahnBanach.thy
--- a/src/HOL/Real/HahnBanach/HahnBanach.thy	Wed Jan 05 20:49:37 2000 +0100
+++ b/src/HOL/Real/HahnBanach/HahnBanach.thy	Thu Jan 06 16:00:18 2000 +0100
@@ -109,7 +109,7 @@
       $E$, which is a superspace of $F$. $h$ is an extension of $f$
       and $h$ is again bounded by $p$. *};
 
-      obtain H h in "graph H h = g" and "is_linearform H h" 
+      obtain H h where "graph H h = g" "is_linearform H h" 
         "is_subspace H E" "is_subspace F H" "graph F f <= graph H h" 
         "ALL x:H. h x <= p x";
       proof -;
@@ -136,7 +136,7 @@
 
 	  txt {* Consider $x_0 \in E \setminus H$. *};
 
-          obtain x0 in "x0:E" "x0~:H"; 
+          obtain x0 where "x0:E" "x0~:H"; 
           proof -;
             have "EX x0:E. x0~:H";
             proof (rule set_less_imp_diff_not_empty);
@@ -161,7 +161,7 @@
 	    inequations, which will be used to establish that $h_0$ is
 	    a norm-preserving extension of $h$. *};
 
-            obtain xi in "ALL y:H. - p (y + x0) - h y <= xi 
+            obtain xi where "ALL y:H. - p (y + x0) - h y <= xi 
                               & xi <= p (y + x0) - h y";
             proof -;
 	      from h; have "EX xi. ALL y:H. - p (y + x0) - h y <= xi 
diff -r ce4bb031d664 -r aca11f954993 src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Wed Jan 05 20:49:37 2000 +0100
+++ b/src/Pure/Isar/obtain.ML	Thu Jan 06 16:00:18 2000 +0100
@@ -137,10 +137,11 @@
     K.prf_asm_goal
     (Scan.optional
       (P.and_list1 (Scan.repeat1 P.name -- Scan.option (P.$$$ "::" |-- P.typ) -- P.marg_comment)
-        --| P.$$$ "in") [] --
+        --| P.$$$ "where") [] --
       P.and_list1 ((P.opt_thm_name ":" -- Scan.repeat1 P.propp >> P.triple1) -- P.marg_comment)
     >> (Toplevel.print oo (Toplevel.proof o obtain)));
 
+val _ = OuterSyntax.add_keywords ["where"];
 val _ = OuterSyntax.add_parsers [obtainP];
 
 end;