| changeset 17914 | 99ead7a7eb42 |
| parent 12327 | 5a4d78204492 |
| child 27015 | f8537d69f514 |
| 17913:4159e1523ad8 | 17914:99ead7a7eb42 |
|---|---|
1 (*<*)theory "types" = Main:(*>*) |
1 (*<*)theory "types" imports Main begin(*>*) |
2 types number = nat |
2 types number = nat |
3 gate = "bool \<Rightarrow> bool \<Rightarrow> bool" |
3 gate = "bool \<Rightarrow> bool \<Rightarrow> bool" |
4 ('a,'b)alist = "('a \<times> 'b)list" |
4 ('a,'b)alist = "('a \<times> 'b)list" |
5 |
5 |
6 text{*\noindent |
6 text{*\noindent |