adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

infoflow: Remove a find_theorems invocation.

This commit is contained in:
Matthew Fernandez 2015-11-25 10:30:29 +11:00
parent d9154d00af
commit 24aaad4f8b
1 changed files with 0 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
proof/infoflow/Noninterference_Base_Enabledness_weak_asym.thy
View File

@ -333,10 +333,6 @@ locale noninterference_policy =
context noninterference_policy begin
thm uwr_equiv_rel
find_theorems name: equiv_def
abbreviation uwr2 :: "'s \<Rightarrow> 'd \<Rightarrow> 's \<Rightarrow> bool" ("(_/ \<sim>_\<sim>/ _)" [50,100,50] 1000)
where "s \<sim>u\<sim> t \<equiv> (s,t) \<in> uwr u"