src/HOL/Bali/Term.thy
changeset 13358 c837ba4cfb62
parent 13345 bd611943cbc2
child 13384 a34e38154413
     1.1 --- a/src/HOL/Bali/Term.thy	Sun Jul 14 19:59:55 2002 +0200
     1.2 +++ b/src/HOL/Bali/Term.thy	Mon Jul 15 10:41:34 2002 +0200
     1.3 @@ -106,37 +106,33 @@
     1.4    "sig" <= (type) "\<lparr>name::mname,parTs::ty list,\<dots>::'a\<rparr>"
     1.5  
     1.6  -- "function codes for unary operations"
     1.7 -datatype unop =  UPlus    -- {*{\tt +} unary plus*} 
     1.8 -               | UMinus   -- {*{\tt -} unary minus*}
     1.9 -               | UBitNot  -- {*{\tt ~} bitwise NOT*}
    1.10 -               | UNot     -- {*{\tt !} logical complement*}
    1.11 +datatype unop =  UPlus    
    1.12 +               | UMinus   
    1.13 +               | UBitNot  
    1.14 +               | UNot     
    1.15  
    1.16  -- "function codes for binary operations"
    1.17 -datatype binop = Mul     -- {*{\tt * }   multiplication*}
    1.18 -               | Div     -- {*{\tt /}   division*}
    1.19 -               | Mod     -- {*{\tt %}   remainder*}
    1.20 -               | Plus    -- {*{\tt +}   addition*}
    1.21 -               | Minus   -- {*{\tt -}   subtraction*}
    1.22 -               | LShift  -- {*{\tt <<}  left shift*}
    1.23 -               | RShift  -- {*{\tt >>}  signed right shift*}
    1.24 -               | RShiftU -- {*{\tt >>>} unsigned right shift*}
    1.25 -               | Less    -- {*{\tt <}   less than*}
    1.26 -               | Le      -- {*{\tt <=}  less than or equal*}
    1.27 -               | Greater -- {*{\tt >}   greater than*}
    1.28 -               | Ge      -- {*{\tt >=}  greater than or equal*}
    1.29 -               | Eq      -- {*{\tt ==}  equal*}
    1.30 -               | Neq     -- {*{\tt !=}  not equal*}
    1.31 -               | BitAnd  -- {*{\tt &}   bitwise AND*}
    1.32 -               | And     -- {*{\tt &}   boolean AND*}
    1.33 -               | BitXor  -- {*{\tt ^}   bitwise Xor*}
    1.34 -               | Xor     -- {*{\tt ^}   boolean Xor*}
    1.35 -               | BitOr   -- {*{\tt |}   bitwise Or*}
    1.36 -               | Or      -- {*{\tt |}   boolean Or*}
    1.37 -text{* The boolean operators {\tt &} and {\tt |} strictly evaluate both
    1.38 -of their arguments. The lazy operators {\tt &&} and {\tt ||} are modeled
    1.39 -as instances of the @{text Cond} expression: {\tt a && b = a?b:false} and
    1.40 -  {\tt a || b = a?true:b}
    1.41 -*}
    1.42 +datatype binop = Mul     
    1.43 +               | Div     
    1.44 +               | Mod     
    1.45 +               | Plus    
    1.46 +               | Minus   
    1.47 +               | LShift  
    1.48 +               | RShift  
    1.49 +               | RShiftU 
    1.50 +               | Less    
    1.51 +               | Le      
    1.52 +               | Greater 
    1.53 +               | Ge      
    1.54 +               | Eq      
    1.55 +               | Neq     
    1.56 +               | BitAnd  
    1.57 +               | And     
    1.58 +               | BitXor  
    1.59 +               | Xor     
    1.60 +               | BitOr   
    1.61 +               | Or      
    1.62 +
    1.63  datatype var
    1.64  	= LVar                  lname(* local variable (incl. parameters) *)
    1.65          | FVar qtname qtname bool expr vname