# HG changeset patch
# User nipkow
# Date 1380188461 -7200
# Node ID a268daff3e0f69083d4a05c61d5c9d95f18f57a2
# Parent  2c5055a3583d456422d3af8294b9d4ab67e275f0
tuned

diff -r 2c5055a3583d -r a268daff3e0f src/HOL/IMP/Compiler2.thy
--- a/src/HOL/IMP/Compiler2.thy	Thu Sep 26 10:57:39 2013 +0200
+++ b/src/HOL/IMP/Compiler2.thy	Thu Sep 26 11:41:01 2013 +0200
@@ -18,22 +18,21 @@
 
 text {* The possible successor PCs of an instruction at position @{term n} *}
 text_raw{*\snip{isuccsdef}{0}{1}{% *}
-definition
-  "isuccs i n \<equiv> case i of 
-     JMP j \<Rightarrow> {n + 1 + j}
-   | JMPLESS j \<Rightarrow> {n + 1 + j, n + 1}
-   | JMPGE j \<Rightarrow> {n + 1 + j, n + 1}
-   | _ \<Rightarrow> {n +1}"
+definition isuccs :: "instr \<Rightarrow> int \<Rightarrow> int set" where
+"isuccs i n = (case i of
+  JMP j \<Rightarrow> {n + 1 + j} |
+  JMPLESS j \<Rightarrow> {n + 1 + j, n + 1} |
+  JMPGE j \<Rightarrow> {n + 1 + j, n + 1} |
+  _ \<Rightarrow> {n +1})"
 text_raw{*}%endsnip*}
 
 text {* The possible successors PCs of an instruction list *}
-definition
-  succs :: "instr list \<Rightarrow> int \<Rightarrow> int set" where
-  "succs P n = {s. \<exists>i::int. 0 \<le> i \<and> i < size P \<and> s \<in> isuccs (P!!i) (n+i)}" 
+definition succs :: "instr list \<Rightarrow> int \<Rightarrow> int set" where
+"succs P n = {s. \<exists>i::int. 0 \<le> i \<and> i < size P \<and> s \<in> isuccs (P!!i) (n+i)}" 
 
 text {* Possible exit PCs of a program *}
-definition
-  "exits P = succs P 0 - {0..< size P}"
+definition exits :: "instr list \<Rightarrow> int set" where
+"exits P = succs P 0 - {0..< size P}"
 
   
 subsection {* Basic properties of @{term exec_n} *}