Theory Operations

section‹Operations›

theory Operations
imports Main
begin

class left_imp = 
  fixes imp_l :: "'a ⇒ 'a ⇒ 'a" (infixr "l→" 65)

class right_imp = 
  fixes imp_r :: "'a ⇒ 'a ⇒ 'a" (infixr "r→" 65)

class left_uminus =
  fixes uminus_l :: "'a => 'a"  ("-l _" [81] 80)

class right_uminus =
  fixes uminus_r :: "'a => 'a"  ("-r _" [81] 80)

end