Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/MicroJava/BV/Err.thy
changeset 11549 e7265e70fd7c
parent 11225 01181fdbc9f0
child 12516 d09d0f160888 
--- a/src/HOL/MicroJava/BV/Err.thy	Tue Sep 04 17:31:18 2001 +0200
+++ b/src/HOL/MicroJava/BV/Err.thy	Tue Sep 04 21:10:57 2001 +0200
@@ -257,7 +257,7 @@
     [| semilat (A,r,f); x +_f y <=_r z; x:A; y:A; z:A |] 
     ==> x <=_r z \<and> y <=_r z"
     by (rule plus_le_conv [THEN iffD1])
-  case antecedent
+  case rule_context
   thus ?thesis
   apply (rule_tac iffI)
    apply clarify
isabelle