1(*
2 * Copyright 2014, General Dynamics C4 Systems
3 *
4 * This software may be distributed and modified according to the terms of
5 * the GNU General Public License version 2. Note that NO WARRANTY is provided.
6 * See "LICENSE_GPLv2.txt" for details.
7 *
8 * @TAG(GD_GPL)
9 *)
10
11(*
12Formalisation of interrupt handling.
13*)
14
15chapter "Arch-specific Interrupts"
16
17theory ArchInterrupt_A
18imports "../Ipc_A"
19begin
20
21
22definition handle_reserved_irq :: "irq \<Rightarrow> (unit,'z::state_ext) s_monad"
23  where "handle_reserved_irq irq = return ()"
24
25
26end
27