equal
deleted
inserted
replaced
36 subsubsection \<open>Syntactic Definitions\<close> |
36 subsubsection \<open>Syntactic Definitions\<close> |
37 |
37 |
38 abbreviation (in ring) dependent :: "'a set \<Rightarrow> 'a list \<Rightarrow> bool" |
38 abbreviation (in ring) dependent :: "'a set \<Rightarrow> 'a list \<Rightarrow> bool" |
39 where "dependent K U \<equiv> \<not> independent K U" |
39 where "dependent K U \<equiv> \<not> independent K U" |
40 |
40 |
41 definition over :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" (infixl "over" 65) |
41 definition over :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" (infixl \<open>over\<close> 65) |
42 where "f over a = f a" |
42 where "f over a = f a" |
43 |
43 |
44 |
44 |
45 |
45 |
46 context ring |
46 context ring |