src/HOL/Bali/Example.thy
changeset 61424 c3658c18b7bc
parent 61337 4645502c3c64
child 62042 6c6ccf573479
     1.1 --- a/src/HOL/Bali/Example.thy	Tue Oct 13 09:21:14 2015 +0200
     1.2 +++ b/src/HOL/Bali/Example.thy	Tue Oct 13 09:21:15 2015 +0200
     1.3 @@ -1247,7 +1247,7 @@
     1.4  abbreviation "s9' == (Some (Xcpt (Std IndOutBound)), s8)"
     1.5  
     1.6  
     1.7 -declare Pair_eq [simp del]
     1.8 +declare prod.inject [simp del]
     1.9  schematic_goal exec_test: 
    1.10  "\<lbrakk>the (new_Addr (heap  s1)) = a;  
    1.11    the (new_Addr (heap ?s2)) = b;  
    1.12 @@ -1377,6 +1377,6 @@
    1.13  apply  (simp (no_asm_simp))
    1.14  apply (auto simp add: in_bounds_def)
    1.15  done
    1.16 -declare Pair_eq [simp]
    1.17 +declare prod.inject [simp]
    1.18  
    1.19  end