equal
deleted
inserted
replaced
42 prop_rec :: "[i, i, i=>i, [i,i,i,i]=>i] => i" |
42 prop_rec :: "[i, i, i=>i, [i,i,i,i]=>i] => i" |
43 is_true :: "[i,i] => o" |
43 is_true :: "[i,i] => o" |
44 "|=" :: "[i,i] => o" (infixl 50) |
44 "|=" :: "[i,i] => o" (infixl 50) |
45 hyps :: "[i,i] => i" |
45 hyps :: "[i,i] => i" |
46 |
46 |
47 rules |
47 defs |
48 |
48 |
49 prop_rec_def |
49 prop_rec_def |
50 "prop_rec(p,b,c,h) == \ |
50 "prop_rec(p,b,c,h) == \ |
51 \ Vrec(p, %p g.prop_case(b, c, %x y. h(x, y, g`x, g`y), p))" |
51 \ Vrec(p, %p g.prop_case(b, c, %x y. h(x, y, g`x, g`y), p))" |
52 |
52 |