changeset 16417 | 9bc16273c2d4 |
parent 13439 | 2f98365f57a8 |
16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
---|---|
1 theory FP0 = PreList: |
1 theory FP0 imports PreList begin |
2 |
2 |
3 datatype 'a list = Nil ("[]") |
3 datatype 'a list = Nil ("[]") |
4 | Cons 'a "'a list" (infixr "#" 65) |
4 | Cons 'a "'a list" (infixr "#" 65) |
5 |
5 |
6 consts app :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "@" 65) |
6 consts app :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "@" 65) |