src/HOL/MicroJava/J/Example.thy
changeset 62145 5b946c81dfbf
parent 62042 6c6ccf573479
child 62390 842917225d56
     1.1 --- a/src/HOL/MicroJava/J/Example.thy	Mon Jan 11 21:20:44 2016 +0100
     1.2 +++ b/src/HOL/MicroJava/J/Example.thy	Mon Jan 11 21:21:02 2016 +0100
     1.3 @@ -82,31 +82,33 @@
     1.4  declare Base_not_Xcpt [symmetric, simp]
     1.5  declare Ext_not_Xcpt  [symmetric, simp]
     1.6  
     1.7 -consts
     1.8 -  foo_Base::  java_mb
     1.9 -  foo_Ext ::  java_mb
    1.10 -  BaseC   :: "java_mb cdecl"
    1.11 -  ExtC    :: "java_mb cdecl"
    1.12 -  test    ::  stmt
    1.13 -  foo   ::  mname
    1.14 -  a   ::  loc
    1.15 -  b       ::  loc
    1.16 +definition foo_Base :: java_mb
    1.17 +  where "foo_Base == ([x],[],Skip,LAcc x)"
    1.18  
    1.19 -defs
    1.20 -  foo_Base_def:"foo_Base == ([x],[],Skip,LAcc x)"
    1.21 -  BaseC_def:"BaseC == (Base, (Object, 
    1.22 +definition foo_Ext :: java_mb
    1.23 +  where "foo_Ext == ([x],[],Expr( {Ext}Cast Ext
    1.24 +               (LAcc x)..vee:=Lit (Intg Numeral1)),
    1.25 +           Lit Null)"
    1.26 +
    1.27 +consts foo ::  mname
    1.28 +
    1.29 +definition BaseC :: "java_mb cdecl"
    1.30 +  where "BaseC == (Base, (Object, 
    1.31             [(vee, PrimT Boolean)], 
    1.32             [((foo,[Class Base]),Class Base,foo_Base)]))"
    1.33 -  foo_Ext_def:"foo_Ext == ([x],[],Expr( {Ext}Cast Ext
    1.34 -               (LAcc x)..vee:=Lit (Intg Numeral1)),
    1.35 -           Lit Null)"
    1.36 -  ExtC_def: "ExtC  == (Ext,  (Base  , 
    1.37 +
    1.38 +definition ExtC :: "java_mb cdecl"
    1.39 +  where "ExtC  == (Ext,  (Base  ,
    1.40             [(vee, PrimT Integer)], 
    1.41             [((foo,[Class Base]),Class Ext,foo_Ext)]))"
    1.42  
    1.43 -  test_def:"test == Expr(e::=NewC Ext);; 
    1.44 +definition test ::  stmt
    1.45 +  where "test == Expr(e::=NewC Ext);;
    1.46                      Expr({Base}LAcc e..foo({[Class Base]}[Lit Null]))"
    1.47  
    1.48 +consts
    1.49 +  a :: loc
    1.50 +  b :: loc
    1.51  
    1.52  abbreviation
    1.53    NP  :: xcpt where