equal
deleted
inserted
replaced
773 |
773 |
774 lemma enclen_zero [simp]: |
774 lemma enclen_zero [simp]: |
775 "enclen 0 = 0" |
775 "enclen 0 = 0" |
776 by (simp add: enclen_def) |
776 by (simp add: enclen_def) |
777 |
777 |
|
778 |
|
779 |
778 section {* Discrete Logarithms *} |
780 section {* Discrete Logarithms *} |
779 |
781 |
780 definition |
782 definition |
781 "rec_lg = |
783 "rec_lg = |
782 (let calc = CN rec_not [CN rec_le [CN rec_power [Id 3 2, Id 3 0], Id 3 1]] in |
784 (let calc = CN rec_not [CN rec_le [CN rec_power [Id 3 2, Id 3 0], Id 3 1]] in |