| changeset 10789 | 260fa2c67e3e |
| parent 10448 | da7d0e28f746 |
| child 13735 | 7de9342aca7a |
--- a/src/HOL/Algebra/abstract/Factor.ML Fri Jan 05 13:10:37 2001 +0100 +++ b/src/HOL/Algebra/abstract/Factor.ML Fri Jan 05 14:28:10 2001 +0100 @@ -5,7 +5,7 @@ *) goalw Ring.thy [assoc_def] "!! c::'a::factorial. \ -\ [| irred c; irred a; irred b; c dvd (a*b) |] ==> c assoc a | c assoc b"; +\ [| irred c; irred a; irred b; c dvd a*b |] ==> c assoc a | c assoc b"; by (ftac factorial_prime 1); by (rewrite_goals_tac [irred_def, prime_def]); by (Blast_tac 1);