equal
deleted
inserted
replaced
109 *} |
109 *} |
110 |
110 |
111 consts |
111 consts |
112 napply :: "[i=>i,i,i]=>i" ("(_ ^ _ ` _)" [56,56,56] 56) |
112 napply :: "[i=>i,i,i]=>i" ("(_ ^ _ ` _)" [56,56,56] 56) |
113 |
113 |
114 axioms |
114 defs |
115 |
|
116 one_def: "one == true" |
115 one_def: "one == true" |
117 if_def: "if b then t else u == case(b,t,u,% x y. bot,%v. bot)" |
116 if_def: "if b then t else u == case(b,t,u,% x y. bot,%v. bot)" |
118 inl_def: "inl(a) == <true,a>" |
117 inl_def: "inl(a) == <true,a>" |
119 inr_def: "inr(b) == <false,b>" |
118 inr_def: "inr(b) == <false,b>" |
120 when_def: "when(t,f,g) == split(t,%b x. if b then f(x) else g(x))" |
119 when_def: "when(t,f,g) == split(t,%b x. if b then f(x) else g(x))" |