# HG changeset patch
# User wenzelm
# Date 931288145 -7200
# Node ID 46652582f8311f0aa7586c2fc6f264755ab40d73
# Parent  9bc05ec3497b0a8ce8a0e97968954ce9fc5af71e
_reflcl;

diff -r 9bc05ec3497b -r 46652582f831 src/HOL/Trancl.thy
--- a/src/HOL/Trancl.thy	Tue Jul 06 21:08:30 1999 +0200
+++ b/src/HOL/Trancl.thy	Tue Jul 06 21:09:05 1999 +0200
@@ -23,7 +23,7 @@
   "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"