--- 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"
--- 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
--- 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;