src/HOL/MicroJava/J/Example.thy
changeset 10042 7164dc0d24d8
parent 9793 2c3d4e03e00c
child 10229 10e2d29a77de
     1.1 --- a/src/HOL/MicroJava/J/Example.thy	Wed Sep 20 21:20:41 2000 +0200
     1.2 +++ b/src/HOL/MicroJava/J/Example.thy	Thu Sep 21 10:42:49 2000 +0200
     1.3 @@ -35,8 +35,8 @@
     1.4  
     1.5  consts
     1.6  
     1.7 -  cnam_ :: "cnam_ \\<Rightarrow> cname"
     1.8 -  vnam_ :: "vnam_ \\<Rightarrow> vnam"
     1.9 +  cnam_ :: "cnam_ => cname"
    1.10 +  vnam_ :: "vnam_ => vnam"
    1.11  
    1.12  rules (* cnam_ and vnam_ are intended to be isomorphic to cnam and vnam *)
    1.13  
    1.14 @@ -74,18 +74,18 @@
    1.15  
    1.16  defs
    1.17  
    1.18 -  foo_Base_def "foo_Base \\<equiv> ([x],[],Skip,LAcc x)"
    1.19 -  BaseC_def "BaseC \\<equiv> (Base, (Some Object, 
    1.20 +  foo_Base_def "foo_Base == ([x],[],Skip,LAcc x)"
    1.21 +  BaseC_def "BaseC == (Base, (Some Object, 
    1.22  			     [(vee, PrimT Boolean)], 
    1.23  			     [((foo,[Class Base]),Class Base,foo_Base)]))"
    1.24 -  foo_Ext_def "foo_Ext \\<equiv> ([x],[],Expr( {Ext}Cast Ext
    1.25 +  foo_Ext_def "foo_Ext == ([x],[],Expr( {Ext}Cast Ext
    1.26  				       (LAcc x)..vee:=Lit (Intg #1)),
    1.27  				   Lit Null)"
    1.28 -  ExtC_def  "ExtC  \\<equiv> (Ext,  (Some Base  , 
    1.29 +  ExtC_def  "ExtC  == (Ext,  (Some Base  , 
    1.30  			     [(vee, PrimT Integer)], 
    1.31  			     [((foo,[Class Base]),Class Ext,foo_Ext)]))"
    1.32  
    1.33 -  test_def "test \\<equiv> Expr(e\\<Colon>=NewC Ext);; 
    1.34 +  test_def "test == Expr(e::=NewC Ext);; 
    1.35                      Expr(LAcc e..foo({[Class Base]}[Lit Null]))"
    1.36  
    1.37