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/Bali/TypeRel.thy
changeset 67613 ce654b0e6d69
parent 67443 3abf6a722518 
--- a/src/HOL/Bali/TypeRel.thy	Tue Feb 13 14:24:50 2018 +0100
+++ b/src/HOL/Bali/TypeRel.thy	Thu Feb 15 12:11:00 2018 +0100
@@ -43,7 +43,7 @@
 
 abbreviation
   subint_syntax :: "prog => [qtname, qtname] => bool" ("_\<turnstile>_\<preceq>I _"  [71,71,71] 70)
-  where "G\<turnstile>I \<preceq>I J == (I,J) \<in>(subint1 G)^*" \<comment> \<open>cf. 9.1.3\<close>
+  where "G\<turnstile>I \<preceq>I J == (I,J) \<in>(subint1 G)\<^sup>*" \<comment> \<open>cf. 9.1.3\<close>
 
 abbreviation
   implmt1_syntax :: "prog => [qtname, qtname] => bool" ("_\<turnstile>_\<leadsto>1_"  [71,71,71] 70)
@@ -116,7 +116,7 @@
 apply (auto intro: rtrancl_into_trancl3)
 done
 
-lemma subcls_is_class: "(C,D) \<in> (subcls1 G)^+ \<Longrightarrow> is_class G C"
+lemma subcls_is_class: "(C,D) \<in> (subcls1 G)\<^sup>+ \<Longrightarrow> is_class G C"
 apply (erule trancl_trans_induct)
 apply (auto dest!: subcls1D)
 done
isabelle