Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned whitespace;
authorwenzelm
Sat, 18 Jul 2015 20:53:05 +0200
changeset 60753 80ca4a065a48
parent 60752 b48830b670a1
child 60754 02924903a6fd
tuned whitespace;
src/HOL/HOLCF/Domain.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/HOLCF/Domain.thy	Sat Jul 18 20:47:08 2015 +0200
+++ b/src/HOL/HOLCF/Domain.thy	Sat Jul 18 20:53:05 2015 +0200
@@ -142,12 +142,12 @@
 
 setup {*
   fold Sign.add_const_constraint
-  [ (@{const_name defl}, SOME @{typ "'a::domain itself \<Rightarrow> udom defl"})
-  , (@{const_name emb}, SOME @{typ "'a::domain \<rightarrow> udom"})
-  , (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::domain"})
-  , (@{const_name liftdefl}, SOME @{typ "'a::predomain itself \<Rightarrow> udom u defl"})
-  , (@{const_name liftemb}, SOME @{typ "'a::predomain u \<rightarrow> udom u"})
-  , (@{const_name liftprj}, SOME @{typ "udom u \<rightarrow> 'a::predomain u"}) ]
+   [(@{const_name defl}, SOME @{typ "'a::domain itself \<Rightarrow> udom defl"}),
+    (@{const_name emb}, SOME @{typ "'a::domain \<rightarrow> udom"}),
+    (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::domain"}),
+    (@{const_name liftdefl}, SOME @{typ "'a::predomain itself \<Rightarrow> udom u defl"}),
+    (@{const_name liftemb}, SOME @{typ "'a::predomain u \<rightarrow> udom u"}),
+    (@{const_name liftprj}, SOME @{typ "udom u \<rightarrow> 'a::predomain u"})]
 *}
 
 ML_file "Tools/domaindef.ML"
isabelle