# HG changeset patch
# User streckem
# Date 1001936029 -7200
# Node ID 0b3a02daf7fb1a74b42f50ec445583b466f0e665
# Parent  352bfe4e1ec020bf4343d5922347560d1d151346
Added axiom e~=This to reflect strengthened precond. in rule LAss

diff -r 352bfe4e1ec0 -r 0b3a02daf7fb src/HOL/MicroJava/J/Example.thy
--- a/src/HOL/MicroJava/J/Example.thy	Mon Oct 01 13:32:11 2001 +0200
+++ b/src/HOL/MicroJava/J/Example.thy	Mon Oct 01 13:33:49 2001 +0200
@@ -75,9 +75,11 @@
 
   Base_not_Object: "Base \<noteq> Object"
   Ext_not_Object:  "Ext  \<noteq> Object"
+  e_not_This:      "e \<noteq> This"
 
 declare Base_not_Object [simp] Ext_not_Object [simp]
-declare Base_not_Object [THEN not_sym, simp] 
+declare e_not_This [simp]
+declare Base_not_Object [THEN not_sym, simp]
 declare Ext_not_Object  [THEN not_sym, simp]
 
 consts
@@ -329,6 +331,7 @@
 apply (tactic t) (* ;; *)
 apply  (tactic t) (* Expr *)
 apply  (tactic t) (* LAss *)
+apply    simp (* e \<noteq> This *)
 apply    (tactic t) (* LAcc *)
 apply     (simp (no_asm))
 apply    (simp (no_asm))