equal
deleted
inserted
replaced
9 Sprod1 = Sprod0 + |
9 Sprod1 = Sprod0 + |
10 |
10 |
11 consts |
11 consts |
12 less_sprod :: "[('a ** 'b),('a ** 'b)] => bool" |
12 less_sprod :: "[('a ** 'b),('a ** 'b)] => bool" |
13 |
13 |
14 rules |
14 defs |
15 |
15 less_sprod_def "less_sprod p1 p2 == |
16 less_sprod_def "less_sprod(p1,p2) == @z. |
16 if p1 = Ispair UU UU |
17 ( p1=Ispair(UU,UU) --> z = True) |
17 then True |
18 &(~p1=Ispair(UU,UU) --> z = ( Isfst(p1) << Isfst(p2) & |
18 else Isfst p1 << Isfst p2 & Issnd p1 << Issnd p2" |
19 Issnd(p1) << Issnd(p2)))" |
|
20 |
19 |
21 end |
20 end |
22 |
|