src/HOL/MicroJava/JVM/Method.ML
changeset 8011 d14c4e9e9c8e
equal deleted inserted replaced
8010:69032a618aa9 8011:d14c4e9e9c8e
       
     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];