diff -r 57e33978e55d -r c92a41d9c4da thys3/src/FBound.thy --- a/thys3/src/FBound.thy Tue Jul 05 00:42:06 2022 +0100 +++ b/thys3/src/FBound.thy Sat Jul 09 14:11:07 2022 +0100 @@ -18,6 +18,7 @@ | "rerase (AALTs bs rs) = RALTS (map rerase rs)" | "rerase (ASEQ _ r1 r2) = RSEQ (rerase r1) (rerase r2)" | "rerase (ASTAR _ r) = RSTAR (rerase r)" +| "rerase (ANTIMES _ r n) = RNTIMES (rerase r) n" lemma eq1_rerase: shows "x ~1 y \ (rerase x) = (rerase y)"