equal
deleted
inserted
replaced
19 inclusion is usually not encountered in plain set-theory. |
19 inclusion is usually not encountered in plain set-theory. |
20 *} |
20 *} |
21 |
21 |
22 lemmas [intro!] = Int_greatest Un_upper2 Un_upper1 Int_lower1 Int_lower2 |
22 lemmas [intro!] = Int_greatest Un_upper2 Un_upper1 Int_lower1 Int_lower2 |
23 |
23 |
24 types 'a ctl = "'a set" |
24 type_synonym 'a ctl = "'a set" |
25 |
25 |
26 definition |
26 definition |
27 imp :: "'a ctl \<Rightarrow> 'a ctl \<Rightarrow> 'a ctl" (infixr "\<rightarrow>" 75) where |
27 imp :: "'a ctl \<Rightarrow> 'a ctl \<Rightarrow> 'a ctl" (infixr "\<rightarrow>" 75) where |
28 "p \<rightarrow> q = - p \<union> q" |
28 "p \<rightarrow> q = - p \<union> q" |
29 |
29 |