equal
deleted
inserted
replaced
1 |
1 |
2 (*** Addition with fixpoint of successor ***) |
2 (* $Id$ *) |
3 |
3 |
4 Ex3 = LCF + |
4 header {* Addition with fixpoint of successor *} |
|
5 |
|
6 theory Ex3 |
|
7 imports LCF |
|
8 begin |
5 |
9 |
6 consts |
10 consts |
7 s :: "'a => 'a" |
11 s :: "'a => 'a" |
8 p :: "'a => 'a => 'a" |
12 p :: "'a => 'a => 'a" |
9 |
13 |
10 rules |
14 axioms |
11 p_strict "p(UU) = UU" |
15 p_strict: "p(UU) = UU" |
12 p_s "p(s(x),y) = s(p(x,y))" |
16 p_s: "p(s(x),y) = s(p(x,y))" |
|
17 |
|
18 ML {* use_legacy_bindings (the_context ()) *} |
13 |
19 |
14 end |
20 end |