src/HOL/Word/Traditional_Syntax.thy

clarified theory data: more robust merge;

(*  Author:     Jeremy Dawson, NICTA
*)

section \<open>Operation variants with traditional syntax\<close>

theory Traditional_Syntax
  imports Main
begin

class semiring_bit_syntax = semiring_bit_shifts +
  fixes test_bit :: \<open>'a \<Rightarrow> nat \<Rightarrow> bool\<close>  (infixl "!!" 100)
    and shiftl :: \<open>'a \<Rightarrow> nat \<Rightarrow> 'a\<close>  (infixl "<<" 55)
    and shiftr :: \<open>'a \<Rightarrow> nat \<Rightarrow> 'a\<close>  (infixl ">>" 55)
  assumes test_bit_eq_bit: \<open>test_bit = bit\<close>
    and shiftl_eq_push_bit: \<open>a << n = push_bit n a\<close>
    and shiftr_eq_drop_bit: \<open>a >> n = drop_bit n a\<close>

end