src/HOL/MicroJava/J/Term.thy
changeset 11070 cc421547e744
parent 11026 a50365d21144
child 12517 360e3215f029
equal deleted inserted replaced
11069:4f6fd393713f 11070:cc421547e744
     1 (*  Title:      HOL/MicroJava/J/Term.thy
     1 (*  Title:      HOL/MicroJava/J/Term.thy
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     David von Oheimb
     3     Author:     David von Oheimb
     4     Copyright   1999 Technische Universitaet Muenchen
     4     Copyright   1999 Technische Universitaet Muenchen
       
     5 *)
     5 
     6 
     6 Java expressions and statements
     7 header "Expressions and Statements"
     7 *)
       
     8 
     8 
     9 theory Term = Value:
     9 theory Term = Value:
    10 
    10 
    11 datatype binop = Eq | Add    (* function codes for binary operation *)
    11 datatype binop = Eq | Add    (* function codes for binary operation *)
    12 
    12