diff -r aea02b5a58d2 -r 6e7244ae43b8 thys/UF_Rec.thy --- a/thys/UF_Rec.thy Thu May 02 12:49:33 2013 +0100 +++ b/thys/UF_Rec.thy Thu May 02 13:19:50 2013 +0100 @@ -95,7 +95,7 @@ "Scan r = r mod 2" definition - "rec_scan = CN rec_rem [Id 1 0, constn 2]" + "rec_scan = CN rec_mod [Id 1 0, constn 2]" lemma scan_lemma [simp]: "rec_eval rec_scan [r] = r mod 2" @@ -124,7 +124,7 @@ let cond2 = CN rec_eq [Id 3 2, constn 2] in let cond3 = CN rec_eq [Id 3 2, constn 3] in let case3 = CN rec_add [CN rec_mult [constn 2, Id 3 0], - CN rec_rem [Id 3 1, constn 2]] in + CN rec_mod [Id 3 1, constn 2]] in CN rec_if [cond1, Id 3 0, CN rec_if [cond2, CN rec_quo [Id 3 0, constn 2], CN rec_if [cond3, case3, Id 3 0]]])" @@ -135,7 +135,7 @@ let case0 = CN rec_minus [Id 3 1, CN rec_scan [Id 3 1]] in let case1 = CN rec_minus [CN rec_add [Id 3 1, constn 1], CN rec_scan [Id 3 1]] in let case2 = CN rec_add [CN rec_mult [constn 2, Id 3 1], - CN rec_rem [Id 3 0, constn 2]] in + CN rec_mod [Id 3 0, constn 2]] in let case3 = CN rec_quo [Id 2 1, constn 2] in CN rec_if [condn 0, case0, CN rec_if [condn 1, case1,