src/HOL/MicroJava/BV/StepMono.thy
 changeset 10042 7164dc0d24d8 parent 9941 fe05af7ec816 child 10496 f2d304bdf3cc
```     1.1 --- a/src/HOL/MicroJava/BV/StepMono.thy	Wed Sep 20 21:20:41 2000 +0200
1.2 +++ b/src/HOL/MicroJava/BV/StepMono.thy	Thu Sep 21 10:42:49 2000 +0200
1.3 @@ -14,7 +14,7 @@
1.4
1.5
1.6  lemma sup_loc_some [rule_format]:
1.7 -"\<forall> y n. (G \<turnstile> b <=l y) \<longrightarrow> n < length y \<longrightarrow> y!n = Ok t \<longrightarrow>
1.8 +"\<forall> y n. (G \<turnstile> b <=l y) --> n < length y --> y!n = Ok t -->
1.9    (\<exists>t. b!n = Ok t \<and> (G \<turnstile> (b!n) <=o (y!n)))" (is "?P b")
1.10  proof (induct (open) ?P b)
1.11    show "?P []" by simp
1.12 @@ -41,9 +41,9 @@
1.13
1.14
1.15  lemma all_widen_is_sup_loc:
1.16 -"\<forall>b. length a = length b \<longrightarrow>
1.17 +"\<forall>b. length a = length b -->
1.18       (\<forall>x\<in>set (zip a b). x \<in> widen G) = (G \<turnstile> (map Ok a) <=l (map Ok b))"
1.19 - (is "\<forall>b. length a = length b \<longrightarrow> ?Q a b" is "?P a")
1.20 + (is "\<forall>b. length a = length b --> ?Q a b" is "?P a")
1.21  proof (induct "a")
1.22    show "?P []" by simp
1.23
1.24 @@ -60,7 +60,7 @@
1.25
1.26
1.27  lemma append_length_n [rule_format]:
1.28 -"\<forall>n. n \<le> length x \<longrightarrow> (\<exists>a b. x = a@b \<and> length a = n)" (is "?P x")
1.29 +"\<forall>n. n \<le> length x --> (\<exists>a b. x = a@b \<and> length a = n)" (is "?P x")
1.30  proof (induct (open) ?P x)
1.31    show "?P []" by simp
1.32
1.33 @@ -94,7 +94,7 @@
1.34
1.35
1.36  lemma rev_append_cons:
1.37 -"\<lbrakk>n < length x\<rbrakk> \<Longrightarrow> \<exists>a b c. x = (rev a) @ b # c \<and> length a = n"
1.38 +"[|n < length x|] ==> \<exists>a b c. x = (rev a) @ b # c \<and> length a = n"
1.39  proof -
1.40    assume n: "n < length x"
1.41    hence "n \<le> length x" by simp
1.42 @@ -118,7 +118,7 @@
1.43
1.44
1.45  lemma app_mono:
1.46 -"\<lbrakk>G \<turnstile> s <=' s'; app i G rT s'\<rbrakk> \<Longrightarrow> app i G rT s";
1.47 +"[|G \<turnstile> s <=' s'; app i G rT s'|] ==> app i G rT s";
1.48  proof -
1.49
1.50    { fix s1 s2
```