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/NSA/StarDef.thy
changeset 62378 85ed00c1fe7c
parent 62376 85f38d5f8807 
--- a/src/HOL/NSA/StarDef.thy	Fri Feb 12 16:09:07 2016 +0100
+++ b/src/HOL/NSA/StarDef.thy	Fri Feb 19 13:40:50 2016 +0100
@@ -987,7 +987,8 @@
 lemma star_of_of_int [simp]: "star_of (of_int z) = of_int z"
 by transfer (rule refl)
 
-instance star :: (semiring_char_0) semiring_char_0 proof
+instance star :: (semiring_char_0) semiring_char_0
+proof
   have "inj (star_of :: 'a \<Rightarrow> 'a star)" by (rule injI) simp
   then have "inj (star_of \<circ> of_nat :: nat \<Rightarrow> 'a star)" using inj_of_nat by (rule inj_comp)
   then show "inj (of_nat :: nat \<Rightarrow> 'a star)" by (simp add: comp_def)
isabelle