summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | Manuel Eberl <eberlm@in.tum.de> |

Sat, 09 Jan 2021 15:56:09 +0100 | |

changeset 73114 | 9bf36baa8686 |

parent 73113 | 918f6c8b1f15 |

child 73115 | a8e5d7c9a834 |

Corrected lemma that was too specific in HOL-Computational_Algebra

--- a/src/HOL/Computational_Algebra/Polynomial.thy Sat Jan 09 00:53:06 2021 +0100 +++ b/src/HOL/Computational_Algebra/Polynomial.thy Sat Jan 09 15:56:09 2021 +0100 @@ -3033,7 +3033,7 @@ and algebraic_int_1 [simp, intro]: "algebraic_int 1" and algebraic_int_numeral [simp, intro]: "algebraic_int (numeral n)" and algebraic_int_of_nat [simp, intro]: "algebraic_int (of_nat k)" - and algebraic_int_of_int [simp, intro]: "algebraic_int (of_int k)" + and algebraic_int_of_int [simp, intro]: "algebraic_int (of_int m)" by (simp_all add: int_imp_algebraic_int) lemma algebraic_int_ii [simp, intro]: "algebraic_int \<i>"