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/Library/OptionalSugar.thy
changeset 81136 2b949a3bfaac
parent 80914 d97fdabd9e2b 
--- a/src/HOL/Library/OptionalSugar.thy	Tue Oct 08 23:31:06 2024 +0200
+++ b/src/HOL/Library/OptionalSugar.thy	Wed Oct 09 13:06:55 2024 +0200
@@ -51,14 +51,7 @@
   "_bind (p # CONST DUMMY) e" <= "_bind p (CONST hd e)"
   "_bind (CONST DUMMY # p) e" <= "_bind p (CONST tl e)"
 
-(* 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
 
 
 (* sorts as intersections *)
isabelle