src/HOL/MicroJava/J/Term.thy
changeset 16417 9bc16273c2d4
parent 12911 704713ca07ea
child 41589 bbd861837ebc
equal deleted inserted replaced
16416:6061ae1f90f2 16417:9bc16273c2d4
     4     Copyright   1999 Technische Universitaet Muenchen
     4     Copyright   1999 Technische Universitaet Muenchen
     5 *)
     5 *)
     6 
     6 
     7 header {* \isaheader{Expressions and Statements} *}
     7 header {* \isaheader{Expressions and Statements} *}
     8 
     8 
     9 theory Term = Value:
     9 theory Term imports Value begin
    10 
    10 
    11 datatype binop = Eq | Add    -- "function codes for binary operation"
    11 datatype binop = Eq | Add    -- "function codes for binary operation"
    12 
    12 
    13 datatype expr
    13 datatype expr
    14   = NewC cname               -- "class instance creation"
    14   = NewC cname               -- "class instance creation"