diff -r ceb0bdc99893 -r 6c722e960f2e thys/Hoare_tm.thy
--- a/thys/Hoare_tm.thy	Fri Mar 21 21:40:51 2014 +0800
+++ b/thys/Hoare_tm.thy	Fri Mar 21 13:49:20 2014 +0000
@@ -1,5 +1,5 @@
 header {* 
-  Separation logic for TM
+  Separation logic for Turing Machines
 *}
 
 theory Hoare_tm
@@ -23,8 +23,9 @@
 
 lemmas int_add_ac = int_add_A int_add_C int_add_LC
 
-method_setup prune = {* Scan.succeed (SIMPLE_METHOD' o (K (K prune_params_tac))) *} 
-                       "pruning parameters"
+method_setup prune = 
+  {* Scan.succeed (SIMPLE_METHOD' o (K (K prune_params_tac))) *} 
+  "pruning parameters"
 
 ML {*
 structure StepRules = Named_Thms
@@ -110,7 +111,7 @@
 
 interpretation tm: sep_exec tstep trset_of .
 
-section {* Assembly language and its program logic *}
+section {* Assembly language for TMs and its program logic *}
 
 subsection {* The assembly language *}
 
@@ -118,7 +119,7 @@
    TInstr tm_inst
  | TLabel nat
  | TSeq tpg tpg
- | TLocal "(nat \<Rightarrow> tpg)"
+ | TLocal "nat \<Rightarrow> tpg"
 
 notation TLocal (binder "TL " 10)
 
@@ -132,14 +133,12 @@
 
 type_synonym tassert = "tresource set \<Rightarrow> bool"
 
-abbreviation t_hoare :: 
-  "tassert \<Rightarrow> tassert  \<Rightarrow> tassert \<Rightarrow> bool" ("(\<lbrace>(1_)\<rbrace> / (_)/ \<lbrace>(1_)\<rbrace>)" 50)
-  where "\<lbrace> p \<rbrace> c \<lbrace> q \<rbrace> == sep_exec.Hoare_gen tstep trset_of p c q"
+abbreviation t_hoare :: "tassert \<Rightarrow> tassert  \<Rightarrow> tassert \<Rightarrow> bool" ("(\<lbrace>(1_)\<rbrace>/ (_)/ \<lbrace>(1_)\<rbrace>)" 50)
+  where "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace> == sep_exec.Hoare_gen tstep trset_of p c q"
 
 abbreviation it_hoare ::
-  "(('a::sep_algebra) \<Rightarrow> tresource set \<Rightarrow> bool) \<Rightarrow> 
-      ('a \<Rightarrow> bool) \<Rightarrow> (tresource set \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
-  ("(1_).(\<lbrace>(1_)\<rbrace> / (_)/ \<lbrace>(1_)\<rbrace>)" 50)
+  "('a::sep_algebra \<Rightarrow> tresource set \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> (tresource set \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
+      ("(1_).(\<lbrace>(1_)\<rbrace>/ (_)/ \<lbrace>(1_)\<rbrace>)" 50)
 where "I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace> == sep_exec.IHoare tstep trset_of I P c Q"
 
 (*
@@ -147,7 +146,8 @@
   "tpg_len (TInstr ai) = 1" |
   "tpg_len (TSeq p1 p2) = tpg_len p1 + tpg_len " |
   "tpg_len (TLocal fp) = tpg_len (fp 0)" |
-  "tpg_len (TLabel l) = 0" *)
+  "tpg_len (TLabel l) = 0" 
+*)
 
 primrec tassemble_to :: "tpg \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> tassert" 
   where 
@@ -165,7 +165,7 @@
 
 lemma EXS_intro: 
   assumes h: "(P x) s"
-  shows "((EXS x. P(x))) s"
+  shows "(EXS x. P(x)) s"
   by (smt h pred_ex_def sep_conj_impl)
 
 lemma EXS_elim: