equal
deleted
inserted
replaced
46 \<close> |
46 \<close> |
47 |
47 |
48 definition liff :: "[o, o] \<Rightarrow> o" (infixr \<open>o-o\<close> 45) |
48 definition liff :: "[o, o] \<Rightarrow> o" (infixr \<open>o-o\<close> 45) |
49 where "P o-o Q == (P -o Q) >< (Q -o P)" |
49 where "P o-o Q == (P -o Q) >< (Q -o P)" |
50 |
50 |
51 definition aneg :: "o\<Rightarrow>o" (\<open>~_\<close>) |
51 definition aneg :: "o\<Rightarrow>o" (\<open>(\<open>open_block notation=\<open>prefix ~\<close>\<close>~_)\<close>) |
52 where "~A == A -o 0" |
52 where "~A == A -o 0" |
53 |
53 |
54 |
54 |
55 axiomatization where |
55 axiomatization where |
56 |
56 |