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/HOLCF/IOA/meta_theory/CompoTraces.thy
changeset 58318 f95754ca7082
parent 48194 1440a3103af0
child 58880 0baae4311a9f 
--- a/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy	Thu Sep 11 20:01:29 2014 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy	Thu Sep 11 21:11:03 2014 +0200
@@ -563,7 +563,7 @@
 apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
 apply (erule conjE)+
 
-(* subst divide_Seq in conclusion, but only at the righest occurence *)
+(* subst divide_Seq in conclusion, but only at the righest occurrence *)
 apply (rule_tac t = "schA" in ssubst)
 back
 back
@@ -616,7 +616,7 @@
 apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
 apply (erule conjE)+
 
-(* subst divide_Seq in conclusion, but only at the righest occurence *)
+(* subst divide_Seq in conclusion, but only at the rightmost occurrence *)
 apply (rule_tac t = "schA" in ssubst)
 back
 back
@@ -782,7 +782,7 @@
 apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
 apply (erule conjE)+
 
-(* subst divide_Seq in conclusion, but only at the righest occurence *)
+(* subst divide_Seq in conclusion, but only at the rightmost occurrence *)
 apply (rule_tac t = "schB" in ssubst)
 back
 back
@@ -833,7 +833,7 @@
 apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
 apply (erule conjE)+
 
-(* subst divide_Seq in conclusion, but only at the righest occurence *)
+(* subst divide_Seq in conclusion, but only at the rightmost occurrence *)
 apply (rule_tac t = "schB" in ssubst)
 back
 back
isabelle