Mercurial Mercurial > hg > pip / 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.
Correctness.thy
changeset 122 420e03a2d9cc
parent 116 a7441db6f4e1
child 125 95e7933968f8 
--- a/Correctness.thy	Mon Mar 21 14:41:40 2016 +0000
+++ b/Correctness.thy	Mon Mar 21 15:06:52 2016 +0000
@@ -49,7 +49,7 @@
 
 -- {* @{term s} is a valid trace, so it will inherit all results derived for
       a valid trace: *}
-sublocale highest_gen < vat_s: valid_trace "s"
+sublocale highest_gen < vat_s?: valid_trace "s"
   by (unfold_locales, insert vt_s, simp)
 
 context highest_gen
@@ -98,7 +98,7 @@
   and set_diff_low: "Set th' prio' \<in> set t \<Longrightarrow> th' \<noteq> th \<and> prio' \<le> prio"
   and exit_diff: "Exit th' \<in> set t \<Longrightarrow> th' \<noteq> th"
 
-sublocale extend_highest_gen < vat_t: valid_trace "t@s"
+sublocale extend_highest_gen < vat_t?: valid_trace "t@s"
   by (unfold_locales, insert vt_t, simp)
 
 lemma step_back_vt_app:
pip