(* lemmas relevant to logical rules ands_rep, ora_rep *) IrepI = Igen + GRepm + consts bsStar :: "structr => structr" primrec "bsStar (Comma X Y) = Comma (Star X) (Star Y)" "bsStar (Star X) = X" "bsStar I = Star I" (* otherwise, need more than aidps *) "bsStar (Structform f) = Star (Structform f)" "bsStar (SV s) = Star (SV s)" end