# HG changeset patch
# User wenzelm
# Date 936213890 -7200
# Node ID e0be36ee7ab9d6c7b6650b45829979d1d2af79cf
# Parent  2089c70f2c6d7ae4f494b9b568e26a50d6ff027a
*: no quotes;

diff -r 2089c70f2c6d -r e0be36ee7ab9 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Sep 01 21:24:23 1999 +0200
+++ b/src/HOL/HOL.thy	Wed Sep 01 21:24:50 1999 +0200
@@ -62,7 +62,7 @@
   "+"           :: "['a::plus, 'a]  => 'a"          (infixl 65)
   -             :: "['a::minus, 'a] => 'a"          (infixl 65)
   uminus        :: "['a::minus] => 'a"              ("- _" [81] 80)
-  "*"           :: "['a::times, 'a] => 'a"          (infixl 70)
+  *             :: "['a::times, 'a] => 'a"          (infixl 70)
   (*See Nat.thy for "^"*)