*: no quotes;
authorwenzelm
Wed Sep 01 21:24:50 1999 +0200 (1999-09-01)
changeset 7426e0be36ee7ab9
parent 7425 2089c70f2c6d
child 7427 e5a5d59dd513
*: no quotes;
src/HOL/HOL.thy
     1.1 --- a/src/HOL/HOL.thy	Wed Sep 01 21:24:23 1999 +0200
     1.2 +++ b/src/HOL/HOL.thy	Wed Sep 01 21:24:50 1999 +0200
     1.3 @@ -62,7 +62,7 @@
     1.4    "+"           :: "['a::plus, 'a]  => 'a"          (infixl 65)
     1.5    -             :: "['a::minus, 'a] => 'a"          (infixl 65)
     1.6    uminus        :: "['a::minus] => 'a"              ("- _" [81] 80)
     1.7 -  "*"           :: "['a::times, 'a] => 'a"          (infixl 70)
     1.8 +  *             :: "['a::times, 'a] => 'a"          (infixl 70)
     1.9    (*See Nat.thy for "^"*)
    1.10  
    1.11