1.1 --- a/src/HOL/Isar_examples/W_correct.thy	Wed Jan 05 20:49:37 2000 +0100
     1.2 +++ b/src/HOL/Isar_examples/W_correct.thy	Thu Jan 06 16:00:18 2000 +0100
     1.3 @@ -113,7 +113,7 @@
     1.4        fix a s t m n;
     1.5        assume "Ok (s, t, m) = W (Abs e) a n";
     1.6        thus "$ s a |- Abs e :: t";
     1.7 -	obtain t' in "t = s n -> t'" "Ok (s, t', m) = W e (TVar n # a) (Suc n)";
     1.8 +	obtain t' where "t = s n -> t'" "Ok (s, t', m) = W e (TVar n # a) (Suc n)";
     1.9  	  by (rule rev_mp) simp;
    1.10  	with hyp; show ?thesis; by (force intro: has_type.AbsI);
    1.11        qed;
    1.12 @@ -124,7 +124,7 @@
    1.13      proof (intro allI impI);
    1.14        fix a s t m n; assume "Ok (s, t, m) = W (App e1 e2) a n";
    1.15        thus "$ s a |- App e1 e2 :: t";
    1.16 -	obtain s1 t1 n1 s2 t2 n2 u in
    1.17 +	obtain s1 t1 n1 s2 t2 n2 u where
    1.18            s: "s = $ u o $ s2 o s1"
    1.19            and t: "t = u n2"
    1.20            and mgu_ok: "mgu ($ s2 t1) (t2 -> TVar n2) = Ok u"

     2.1 --- a/src/HOL/Real/HahnBanach/HahnBanach.thy	Wed Jan 05 20:49:37 2000 +0100
     2.2 +++ b/src/HOL/Real/HahnBanach/HahnBanach.thy	Thu Jan 06 16:00:18 2000 +0100
     2.3 @@ -109,7 +109,7 @@
     2.4        $E$, which is a superspace of $F$. $h$ is an extension of $f$
     2.5        and $h$ is again bounded by $p$. *};
     2.6  
     2.7 -      obtain H h in "graph H h = g" and "is_linearform H h" 
     2.8 +      obtain H h where "graph H h = g" "is_linearform H h" 
     2.9          "is_subspace H E" "is_subspace F H" "graph F f <= graph H h" 
    2.10          "ALL x:H. h x <= p x";
    2.11        proof -;
    2.12 @@ -136,7 +136,7 @@
    2.13  
    2.14  	  txt {* Consider $x_0 \in E \setminus H$. *};
    2.15  
    2.16 -          obtain x0 in "x0:E" "x0~:H"; 
    2.17 +          obtain x0 where "x0:E" "x0~:H"; 
    2.18            proof -;
    2.19              have "EX x0:E. x0~:H";
    2.20              proof (rule set_less_imp_diff_not_empty);
    2.21 @@ -161,7 +161,7 @@
    2.22  	    inequations, which will be used to establish that $h_0$ is
    2.23  	    a norm-preserving extension of $h$. *};
    2.24  
    2.25 -            obtain xi in "ALL y:H. - p (y + x0) - h y <= xi 
    2.26 +            obtain xi where "ALL y:H. - p (y + x0) - h y <= xi 
    2.27                                & xi <= p (y + x0) - h y";
    2.28              proof -;
    2.29  	      from h; have "EX xi. ALL y:H. - p (y + x0) - h y <= xi 

     3.1 --- a/src/Pure/Isar/obtain.ML	Wed Jan 05 20:49:37 2000 +0100
     3.2 +++ b/src/Pure/Isar/obtain.ML	Thu Jan 06 16:00:18 2000 +0100
     3.3 @@ -137,10 +137,11 @@
     3.4      K.prf_asm_goal
     3.5      (Scan.optional
     3.6        (P.and_list1 (Scan.repeat1 P.name -- Scan.option (P.$$$ "::" |-- P.typ) -- P.marg_comment)
     3.7 -        --| P.$$$ "in") [] --
     3.8 +        --| P.$$$ "where") [] --
     3.9        P.and_list1 ((P.opt_thm_name ":" -- Scan.repeat1 P.propp >> P.triple1) -- P.marg_comment)
    3.10      >> (Toplevel.print oo (Toplevel.proof o obtain)));
    3.11  
    3.12 +val _ = OuterSyntax.add_keywords ["where"];
    3.13  val _ = OuterSyntax.add_parsers [obtainP];
    3.14  
    3.15  end;