equal
deleted
inserted
replaced
644 lemma alpha4list_equivp: "equivp alpha4list" sorry |
644 lemma alpha4list_equivp: "equivp alpha4list" sorry |
645 |
645 |
646 quotient_type |
646 quotient_type |
647 qtrm4 = trm4 / alpha4 and |
647 qtrm4 = trm4 / alpha4 and |
648 qtrm4list = "trm4 list" / alpha4list |
648 qtrm4list = "trm4 list" / alpha4list |
649 by (simp_all add: alpha4_equivp alpha4list_equivp) |
649 by (simp_all add: alpha4_equivp alpha4list_equivp |
650 |
|
651 |
|
652 |
|
653 |
|
654 |
|
655 |
|
656 |
650 |
657 |
651 |
658 datatype rtrm5 = |
652 datatype rtrm5 = |
659 rVr5 "name" |
653 rVr5 "name" |
660 | rAp5 "rtrm5" "rtrm5" |
654 | rAp5 "rtrm5" "rtrm5" |