| changeset 55072 | 8488fdc4ddc0 |
| parent 54680 | 93f6d33a754e |
| child 55888 | cac1add157e8 |
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Mon Jan 20 18:24:56 2014 +0100 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Mon Jan 20 18:24:56 2014 +0100 @@ -12,7 +12,7 @@ suite. *) theory Manual_Nits -imports Main Real "~~/src/HOL/Library/Quotient_Product" "~~/src/HOL/BNF/BNF" +imports Main Real "~~/src/HOL/Library/Quotient_Product" begin chapter {* 2. First Steps *}