src/HOL/MicroJava/ROOT.ML
author haftmann
Fri Jun 11 17:14:02 2010 +0200 (2010-06-11)
changeset 37407 61dd8c145da7
parent 33615 261abc2e3155
child 41413 64cd30d6b0b8
permissions -rwxr-xr-x
declare lex_prod_def [code del]
wenzelm@33615
     1
no_document use_thys ["While_Combinator"];
kleing@10631
     2
wenzelm@33615
     3
use_thys ["MicroJava"];