# HG changeset patch
# User wenzelm
# Date 972491522 -7200
# Node ID 7411e4659d4abf8bb77ba55f0336016bebf7bbe4
# Parent  4362e906b7450c9ba271f4a50d17917ead239309
more "xsymbols" syntax;

diff -r 4362e906b745 -r 7411e4659d4a src/HOL/Record.thy
--- a/src/HOL/Record.thy	Wed Oct 25 18:31:21 2000 +0200
+++ b/src/HOL/Record.thy	Wed Oct 25 18:32:02 2000 +0200
@@ -40,7 +40,7 @@
   "_updates"            :: "[update, updates] => updates"               ("_,/ _")
   "_record_update"      :: "['a, updates] => 'b"                ("_/(3'(| _ |'))" [900,0] 900)
 
-syntax (input)   (* FIXME (xsymbols) *)
+syntax (xsymbols)
   "_record_type"        :: "field_types => type"                        ("(3\<lparr>_\<rparr>)")
   "_record_type_scheme" :: "[field_types, type] => type"        ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)")
   "_record"             :: "fields => 'a"                               ("(3\<lparr>_\<rparr>)")
diff -r 4362e906b745 -r 7411e4659d4a src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Wed Oct 25 18:31:21 2000 +0200
+++ b/src/HOL/Transitive_Closure.thy	Wed Oct 25 18:32:02 2000 +0200
@@ -9,23 +9,27 @@
 trancl  is transitive closure
 reflcl  is reflexive closure
 
-These postfix operators have MAXIMUM PRIORITY, forcing their operands to be
-      atomic.
+These postfix operators have MAXIMUM PRIORITY, forcing their operands
+to be atomic.
 *)
 
 Transitive_Closure = Lfp + Relation + 
 
 constdefs
-  rtrancl :: "('a * 'a)set => ('a * 'a)set"   ("(_^*)" [1000] 999)
-  "r^*  ==  lfp(%s. Id Un (r O s))"
+  rtrancl :: "('a * 'a) set => ('a * 'a) set"    ("(_^*)" [1000] 999)
+  "r^* == lfp (%s. Id Un (r O s))"
 
-  trancl  :: "('a * 'a)set => ('a * 'a)set"   ("(_^+)" [1000] 999)
-  "r^+  ==  r O rtrancl(r)"
+  trancl :: "('a * 'a) set => ('a * 'a) set"    ("(_^+)" [1000] 999)
+  "r^+ ==  r O rtrancl r"
 
 syntax
-  "_reflcl"  :: "('a*'a)set => ('a*'a)set"       ("(_^=)" [1000] 999)
-
+  "_reflcl" :: "('a * 'a) set => ('a * 'a) set"    ("(_^=)" [1000] 999)
 translations
   "r^=" == "r Un Id"
 
+syntax (xsymbols)
+  rtrancl :: "('a * 'a) set => ('a * 'a) set"    ("(_\\<^sup>*)" [1000] 999)
+  trancl :: "('a * 'a) set => ('a * 'a) set"    ("(_\\<^sup>+)" [1000] 999)
+  "_reflcl" :: "('a * 'a) set => ('a * 'a) set"    ("(_\\<^sup>=)" [1000] 999)
+
 end