spec: Remove excessive strings of newlines.
This commit is contained in:
parent
b737c6ba2a
commit
7521fa080b
|
@ -209,26 +209,6 @@ asidRange :: "(asid * asid)"
|
|||
|
||||
consts
|
||||
asidHighBitsOf :: "asid \<Rightarrow> asid"
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
defs archObjSize_def:
|
||||
"archObjSize a\<equiv> (case a of
|
||||
|
|
|
@ -316,10 +316,6 @@ where
|
|||
"ptBits \<equiv> pageBits - 2"
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
(* vmrights instance proofs *)
|
||||
(*<*)
|
||||
instantiation vmrights :: enum begin
|
||||
|
@ -362,150 +358,6 @@ end
|
|||
|
||||
(*>*)
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
definition
|
||||
wordFromPDE :: "pde \<Rightarrow> machine_word"
|
||||
where
|
||||
|
|
|
@ -112,29 +112,6 @@ end
|
|||
|
||||
(*>*)
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
(*>*)
|
||||
definition
|
||||
"capRegister \<equiv> R0"
|
||||
|
@ -338,8 +315,4 @@ end
|
|||
|
||||
(*>*)
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
end
|
||||
|
|
Loading…
Reference in New Issue