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/Imperative_HOL/Overview.thy
changeset 81136 2b949a3bfaac
parent 80914 d97fdabd9e2b 
--- a/src/HOL/Imperative_HOL/Overview.thy	Tue Oct 08 23:31:06 2024 +0200
+++ b/src/HOL/Imperative_HOL/Overview.thy	Wed Oct 09 13:06:55 2024 +0200
@@ -7,14 +7,7 @@
 imports Imperative_HOL "HOL-Library.LaTeXsugar"
 begin
 
-(* type constraints with spacing *)
-no_syntax (output)
-  "_constrain" :: "logic => type => logic"  (\<open>_::_\<close> [4, 0] 3)
-  "_constrain" :: "prop' => type => prop'"  (\<open>_::_\<close> [4, 0] 3)
-
-syntax (output)
-  "_constrain" :: "logic => type => logic"  (\<open>_ :: _\<close> [4, 0] 3)
-  "_constrain" :: "prop' => type => prop'"  (\<open>_ :: _\<close> [4, 0] 3)
+unbundle constrain_space_syntax
 (*>*)
 
 text \<open>
isabelle