1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7(* Title: interoperability between separation algebra theories and l4.verified
8          theories
9   Author: Rafal Kolanski <rafal.kolanski at nicta.com.au>, 2012
10*)
11
12theory Sep_Algebra_L4v
13imports "Sep_Tactics" "Sep_Fold"
14begin
15
16text \<open>
17  Remove anything conflicting with @{text "pred_*"} in lib,
18  e.g. @{text pred_and} vs @{text pred_conj}\<close>
19
20no_notation pred_and (infixr "and" 35)
21no_notation pred_or (infixr "or" 30)
22no_notation pred_not ("not _" [40] 40)
23no_notation pred_imp (infixr "imp" 25)
24
25end
26