equal
deleted
inserted
replaced
15 sinr :: "'b -> ('a++'b)" |
15 sinr :: "'b -> ('a++'b)" |
16 sswhen :: "('a->'c)->('b->'c)->('a ++ 'b)-> 'c" |
16 sswhen :: "('a->'c)->('b->'c)->('a ++ 'b)-> 'c" |
17 |
17 |
18 defs |
18 defs |
19 |
19 |
20 sinl_def "sinl == (LAM x.Isinl(x))" |
20 sinl_def "sinl == (LAM x. Isinl(x))" |
21 sinr_def "sinr == (LAM x.Isinr(x))" |
21 sinr_def "sinr == (LAM x. Isinr(x))" |
22 sswhen_def "sswhen == (LAM f g s.Iwhen(f)(g)(s))" |
22 sswhen_def "sswhen == (LAM f g s. Iwhen(f)(g)(s))" |
23 |
23 |
24 translations |
24 translations |
25 "case s of sinl`x => t1 | sinr`y => t2" == "sswhen`(LAM x.t1)`(LAM y.t2)`s" |
25 "case s of sinl`x => t1 | sinr`y => t2" == "sswhen`(LAM x. t1)`(LAM y. t2)`s" |
26 |
26 |
27 end |
27 end |