Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/HoareParallel/OG_Tran.thy
changeset 30952 7ab2716dd93b
parent 30304 d8e4cd2ac2a1 
--- a/src/HOL/HoareParallel/OG_Tran.thy	Fri Apr 17 16:41:31 2009 +0200
+++ b/src/HOL/HoareParallel/OG_Tran.thy	Mon Apr 20 09:32:07 2009 +0200
@@ -74,7 +74,7 @@
 abbreviation
   ann_transition_n :: "('a ann_com_op \<times> 'a) \<Rightarrow> nat \<Rightarrow> ('a ann_com_op \<times> 'a) 
                            \<Rightarrow> bool"  ("_ -_\<rightarrow> _"[81,81] 100)  where
-  "con_0 -n\<rightarrow> con_1 \<equiv> (con_0, con_1) \<in> ann_transition^n"
+  "con_0 -n\<rightarrow> con_1 \<equiv> (con_0, con_1) \<in> ann_transition ^^ n"
 
 abbreviation
   ann_transitions :: "('a ann_com_op \<times> 'a) \<Rightarrow> ('a ann_com_op \<times> 'a) \<Rightarrow> bool"
@@ -84,7 +84,7 @@
 abbreviation
   transition_n :: "('a com \<times> 'a) \<Rightarrow> nat \<Rightarrow> ('a com \<times> 'a) \<Rightarrow> bool"  
                           ("_ -P_\<rightarrow> _"[81,81,81] 100)  where
-  "con_0 -Pn\<rightarrow> con_1 \<equiv> (con_0, con_1) \<in> transition^n"
+  "con_0 -Pn\<rightarrow> con_1 \<equiv> (con_0, con_1) \<in> transition ^^ n"
 
 subsection {* Definition of Semantics *}
isabelle