changeset 66453 | cc19f7ca2ed6 |
parent 63167 | 0909deb8059b |
child 67346 | 1f1d85393d70 |
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Fri Aug 18 13:55:05 2017 +0200 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Fri Aug 18 20:47:47 2017 +0200 @@ -12,7 +12,7 @@ suite. *) theory Manual_Nits -imports Real "~~/src/HOL/Library/Quotient_Product" +imports HOL.Real "HOL-Library.Quotient_Product" begin section \<open>2. First Steps\<close>