changeset 67123 | 3fe40ff1b921 |
parent 64962 | bf41e1109db3 |
child 67341 | df79ef3b3a41 |
--- a/src/HOL/Decision_Procs/ex/Commutative_Ring_Ex.thy Sun Dec 03 19:09:42 2017 +0100 +++ b/src/HOL/Decision_Procs/ex/Commutative_Ring_Ex.thy Sun Dec 03 22:28:19 2017 +0100 @@ -5,7 +5,7 @@ section \<open>Some examples demonstrating the ring and field methods\<close> theory Commutative_Ring_Ex -imports "../Reflective_Field" + imports "../Reflective_Field" begin lemma "4 * (x::int) ^ 5 * y ^ 3 * x ^ 2 * 3 + x * z + 3 ^ 5 = 12 * x ^ 7 * y ^ 3 + z * x + 243"