Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Added axiom e~=This to reflect strengthened precond. in rule LAss
authorstreckem
Mon, 01 Oct 2001 13:33:49 +0200
changeset 11643 0b3a02daf7fb
parent 11642 352bfe4e1ec0
child 11644 3dfde687f0d7
Added axiom e~=This to reflect strengthened precond. in rule LAss
src/HOL/MicroJava/J/Example.thy file | annotate | diff | comparison | revisions 
--- 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))
isabelle