more "xsymbols" syntax;
authorwenzelm
Wed Oct 25 18:32:02 2000 +0200 (2000-10-25)
changeset 103317411e4659d4a
parent 10330 4362e906b745
child 10332 b4f7f8693f8e
more "xsymbols" syntax;
src/HOL/Record.thy
src/HOL/Transitive_Closure.thy
     1.1 --- a/src/HOL/Record.thy	Wed Oct 25 18:31:21 2000 +0200
     1.2 +++ b/src/HOL/Record.thy	Wed Oct 25 18:32:02 2000 +0200
     1.3 @@ -40,7 +40,7 @@
     1.4    "_updates"            :: "[update, updates] => updates"               ("_,/ _")
     1.5    "_record_update"      :: "['a, updates] => 'b"                ("_/(3'(| _ |'))" [900,0] 900)
     1.6  
     1.7 -syntax (input)   (* FIXME (xsymbols) *)
     1.8 +syntax (xsymbols)
     1.9    "_record_type"        :: "field_types => type"                        ("(3\<lparr>_\<rparr>)")
    1.10    "_record_type_scheme" :: "[field_types, type] => type"        ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)")
    1.11    "_record"             :: "fields => 'a"                               ("(3\<lparr>_\<rparr>)")
     2.1 --- a/src/HOL/Transitive_Closure.thy	Wed Oct 25 18:31:21 2000 +0200
     2.2 +++ b/src/HOL/Transitive_Closure.thy	Wed Oct 25 18:32:02 2000 +0200
     2.3 @@ -9,23 +9,27 @@
     2.4  trancl  is transitive closure
     2.5  reflcl  is reflexive closure
     2.6  
     2.7 -These postfix operators have MAXIMUM PRIORITY, forcing their operands to be
     2.8 -      atomic.
     2.9 +These postfix operators have MAXIMUM PRIORITY, forcing their operands
    2.10 +to be atomic.
    2.11  *)
    2.12  
    2.13  Transitive_Closure = Lfp + Relation + 
    2.14  
    2.15  constdefs
    2.16 -  rtrancl :: "('a * 'a)set => ('a * 'a)set"   ("(_^*)" [1000] 999)
    2.17 -  "r^*  ==  lfp(%s. Id Un (r O s))"
    2.18 +  rtrancl :: "('a * 'a) set => ('a * 'a) set"    ("(_^*)" [1000] 999)
    2.19 +  "r^* == lfp (%s. Id Un (r O s))"
    2.20  
    2.21 -  trancl  :: "('a * 'a)set => ('a * 'a)set"   ("(_^+)" [1000] 999)
    2.22 -  "r^+  ==  r O rtrancl(r)"
    2.23 +  trancl :: "('a * 'a) set => ('a * 'a) set"    ("(_^+)" [1000] 999)
    2.24 +  "r^+ ==  r O rtrancl r"
    2.25  
    2.26  syntax
    2.27 -  "_reflcl"  :: "('a*'a)set => ('a*'a)set"       ("(_^=)" [1000] 999)
    2.28 -
    2.29 +  "_reflcl" :: "('a * 'a) set => ('a * 'a) set"    ("(_^=)" [1000] 999)
    2.30  translations
    2.31    "r^=" == "r Un Id"
    2.32  
    2.33 +syntax (xsymbols)
    2.34 +  rtrancl :: "('a * 'a) set => ('a * 'a) set"    ("(_\\<^sup>*)" [1000] 999)
    2.35 +  trancl :: "('a * 'a) set => ('a * 'a) set"    ("(_\\<^sup>+)" [1000] 999)
    2.36 +  "_reflcl" :: "('a * 'a) set => ('a * 'a) set"    ("(_\\<^sup>=)" [1000] 999)
    2.37 +
    2.38  end