1.1 --- a/src/HOL/IMP/Comp_Rev.thy	Thu Nov 03 15:54:19 2011 +1100
     1.2 +++ b/src/HOL/IMP/Comp_Rev.thy	Thu Nov 03 16:22:29 2011 +1100
     1.3 @@ -18,8 +18,8 @@
     1.4  definition
     1.5    "isuccs i n \<equiv> case i of 
     1.6       JMP j \<Rightarrow> {n + 1 + j}
     1.7 -   | JMPFLESS j \<Rightarrow> {n + 1 + j, n + 1}
     1.8 -   | JMPFGE j \<Rightarrow> {n + 1 + j, n + 1}
     1.9 +   | JMPLESS j \<Rightarrow> {n + 1 + j, n + 1}
    1.10 +   | JMPGE j \<Rightarrow> {n + 1 + j, n + 1}
    1.11     | _ \<Rightarrow> {n +1}"
    1.12  
    1.13  text {* The possible successors pc's of an instruction list *}
    1.14 @@ -88,8 +88,8 @@
    1.15    "succs [LOAD x] n = {n + 1}"
    1.16    "succs [STORE x] n = {n + 1}"
    1.17    "succs [JMP i] n = {n + 1 + i}"
    1.18 -  "succs [JMPFGE i] n = {n + 1 + i, n + 1}"
    1.19 -  "succs [JMPFLESS i] n = {n + 1 + i, n + 1}"
    1.20 +  "succs [JMPGE i] n = {n + 1 + i, n + 1}"
    1.21 +  "succs [JMPLESS i] n = {n + 1 + i, n + 1}"
    1.22    by (auto simp: succs_def isuccs_def)
    1.23  
    1.24  lemma succs_empty [iff]: "succs [] n = {}"
    1.25 @@ -176,8 +176,8 @@
    1.26    "exits [LOAD x] = {1}"
    1.27    "exits [STORE x] = {1}"
    1.28    "i \<noteq> -1 \<Longrightarrow> exits [JMP i] = {1 + i}"
    1.29 -  "i \<noteq> -1 \<Longrightarrow> exits [JMPFGE i] = {1 + i, 1}"
    1.30 -  "i \<noteq> -1 \<Longrightarrow> exits [JMPFLESS i] = {1 + i, 1}"
    1.31 +  "i \<noteq> -1 \<Longrightarrow> exits [JMPGE i] = {1 + i, 1}"
    1.32 +  "i \<noteq> -1 \<Longrightarrow> exits [JMPLESS i] = {1 + i, 1}"
    1.33    by (auto simp: exits_def)
    1.34  
    1.35  lemma acomp_succs [simp]: