equal
deleted
inserted
replaced
12 typedecl 'a list |
12 typedecl 'a list |
13 instance list :: ("term") "term" .. |
13 instance list :: ("term") "term" .. |
14 |
14 |
15 axiomatization |
15 axiomatization |
16 Nil :: "'a list" and |
16 Nil :: "'a list" and |
17 Cons :: "['a, 'a list]=> 'a list" (infixr ":" 60) and |
17 Cons :: "['a, 'a list]=> 'a list" (infixr \<open>:\<close> 60) and |
18 app :: "['a list, 'a list, 'a list] => o" and |
18 app :: "['a list, 'a list, 'a list] => o" and |
19 rev :: "['a list, 'a list] => o" |
19 rev :: "['a list, 'a list] => o" |
20 where |
20 where |
21 appNil: "app(Nil,ys,ys)" and |
21 appNil: "app(Nil,ys,ys)" and |
22 appCons: "app(xs,ys,zs) ==> app(x:xs, ys, x:zs)" and |
22 appCons: "app(xs,ys,zs) ==> app(x:xs, ys, x:zs)" and |