src/HOL/MicroJava/JVM/Method.ML
changeset 8032 1eaae1a2f8ff
parent 8031 826c6222cca2
child 8033 325b8e754523
equal deleted inserted replaced
8031:826c6222cca2 8032:1eaae1a2f8ff
     1 (*  Title:      HOL/MicroJava/JVM/Method.ML
       
     2     ID:         $Id$
       
     3     Author:     Cornelia Pusch
       
     4     Copyright   1999 Technische Universitaet Muenchen
       
     5 *)
       
     6 
       
     7 Addsimps [exec_mr_def];