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 11theory Invocations_R 12imports Invariants_H 13begin 14context begin interpretation Arch . (*FIXME: arch_split*) 15lemma invocation_type_eq[simp]: 16 "invocationType = invocation_type" 17 apply (rule ext) 18 apply (simp add: invocationType_def invocation_type_def Let_def) 19 apply safe 20 apply (frule from_to_enum) 21 apply blast 22 apply (cut_tac x=v in maxBound_is_bound) 23 apply simp 24 done 25end 26declare resolveAddressBits.simps[simp del] 27 28end 29