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.
new-style infix directives
authorpaulson
Sun, 13 Jun 1999 13:53:33 +0200
changeset 6823 97babc436a41
parent 6822 8932f33259d4
child 6824 8f7bfd81a4c6
new-style infix directives
src/HOL/UNITY/Constrains.thy file | annotate | diff | comparison | revisions
src/HOL/UNITY/UNITY.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/UNITY/Constrains.thy	Sun Jun 13 13:52:50 1999 +0200
+++ b/src/HOL/UNITY/Constrains.thy	Sun Jun 13 13:53:33 1999 +0200
@@ -32,7 +32,8 @@
 	   ==> s' : reachable F"
 
 consts
-  Co, Unless :: "['a set, 'a set] => 'a program set"       (infixl 60)
+  Constrains :: "['a set, 'a set] => 'a program set"  (infixl "Co"     60)
+  op_Unless  :: "['a set, 'a set] => 'a program set"  (infixl "Unless" 60)
 
 defs
   Constrains_def
--- a/src/HOL/UNITY/UNITY.thy	Sun Jun 13 13:52:50 1999 +0200
+++ b/src/HOL/UNITY/UNITY.thy	Sun Jun 13 13:53:33 1999 +0200
@@ -15,7 +15,8 @@
   'a program = "{(init:: 'a set, acts :: ('a * 'a)set set). Id:acts}"
 
 consts
-  co, unless :: "['a set, 'a set] => 'a program set"       (infixl 60)
+  constrains :: "['a set, 'a set] => 'a program set"  (infixl "co"     60)
+  op_unless  :: "['a set, 'a set] => 'a program set"  (infixl "unless" 60)
 
 constdefs
     mk_program :: "('a set * ('a * 'a)set set) => 'a program"
isabelle