equal
deleted
inserted
replaced
27 datatype pattern = Pattern |
27 datatype pattern = Pattern |
28 |
28 |
29 definition pat :: "'a \<Rightarrow> pattern" |
29 definition pat :: "'a \<Rightarrow> pattern" |
30 where "pat _ = Pattern" |
30 where "pat _ = Pattern" |
31 |
31 |
32 definition nopat :: "bool \<Rightarrow> pattern" |
32 definition nopat :: "'a \<Rightarrow> pattern" |
33 where "nopat _ = Pattern" |
33 where "nopat _ = Pattern" |
34 |
34 |
35 definition andpat :: "pattern \<Rightarrow> 'a \<Rightarrow> pattern" (infixl "andpat" 60) |
35 definition andpat :: "pattern \<Rightarrow> 'a \<Rightarrow> pattern" (infixl "andpat" 60) |
36 where "_ andpat _ = Pattern" |
36 where "_ andpat _ = Pattern" |
37 |
37 |