# HG changeset patch
# User schirmer
# Date 1026722494 -7200
# Node ID c837ba4cfb62eff87e7040e8b1ffea5abe2d9c5d
# Parent  6f54e992777ed49625e7d16eb2c43b6758daa0c6
fix latex output

diff -r 6f54e992777e -r c837ba4cfb62 src/HOL/Bali/Term.thy
--- a/src/HOL/Bali/Term.thy	Sun Jul 14 19:59:55 2002 +0200
+++ b/src/HOL/Bali/Term.thy	Mon Jul 15 10:41:34 2002 +0200
@@ -106,37 +106,33 @@
   "sig" <= (type) "\<lparr>name::mname,parTs::ty list,\<dots>::'a\<rparr>"
 
 -- "function codes for unary operations"
-datatype unop =  UPlus    -- {*{\tt +} unary plus*} 
-               | UMinus   -- {*{\tt -} unary minus*}
-               | UBitNot  -- {*{\tt ~} bitwise NOT*}
-               | UNot     -- {*{\tt !} logical complement*}
+datatype unop =  UPlus    
+               | UMinus   
+               | UBitNot  
+               | UNot     
 
 -- "function codes for binary operations"
-datatype binop = Mul     -- {*{\tt * }   multiplication*}
-               | Div     -- {*{\tt /}   division*}
-               | Mod     -- {*{\tt %}   remainder*}
-               | Plus    -- {*{\tt +}   addition*}
-               | Minus   -- {*{\tt -}   subtraction*}
-               | LShift  -- {*{\tt <<}  left shift*}
-               | RShift  -- {*{\tt >>}  signed right shift*}
-               | RShiftU -- {*{\tt >>>} unsigned right shift*}
-               | Less    -- {*{\tt <}   less than*}
-               | Le      -- {*{\tt <=}  less than or equal*}
-               | Greater -- {*{\tt >}   greater than*}
-               | Ge      -- {*{\tt >=}  greater than or equal*}
-               | Eq      -- {*{\tt ==}  equal*}
-               | Neq     -- {*{\tt !=}  not equal*}
-               | BitAnd  -- {*{\tt &}   bitwise AND*}
-               | And     -- {*{\tt &}   boolean AND*}
-               | BitXor  -- {*{\tt ^}   bitwise Xor*}
-               | Xor     -- {*{\tt ^}   boolean Xor*}
-               | BitOr   -- {*{\tt |}   bitwise Or*}
-               | Or      -- {*{\tt |}   boolean Or*}
-text{* The boolean operators {\tt &} and {\tt |} strictly evaluate both
-of their arguments. The lazy operators {\tt &&} and {\tt ||} are modeled
-as instances of the @{text Cond} expression: {\tt a && b = a?b:false} and
-  {\tt a || b = a?true:b}
-*}
+datatype binop = Mul     
+               | Div     
+               | Mod     
+               | Plus    
+               | Minus   
+               | LShift  
+               | RShift  
+               | RShiftU 
+               | Less    
+               | Le      
+               | Greater 
+               | Ge      
+               | Eq      
+               | Neq     
+               | BitAnd  
+               | And     
+               | BitXor  
+               | Xor     
+               | BitOr   
+               | Or      
+
 datatype var
 	= LVar                  lname(* local variable (incl. parameters) *)
         | FVar qtname qtname bool expr vname