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 |
650 |
651 |
651 |
652 datatype rtrm5 = |
652 datatype rtrm5 = |
653 rVr5 "name" |
653 rVr5 "name" |
654 | rAp5 "rtrm5" "rtrm5" |
654 | rAp5 "rtrm5" "rtrm5" |