equal
deleted
inserted
replaced
6 *) |
6 *) |
7 |
7 |
8 header {* Boolean Algebras *} |
8 header {* Boolean Algebras *} |
9 |
9 |
10 theory Boolean_Algebra |
10 theory Boolean_Algebra |
11 imports Main |
11 imports PreList |
12 begin |
12 begin |
13 |
13 |
14 locale boolean = |
14 locale boolean = |
15 fixes conj :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<sqinter>" 70) |
15 fixes conj :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<sqinter>" 70) |
16 fixes disj :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<squnion>" 65) |
16 fixes disj :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<squnion>" 65) |