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