src/HOL/Nitpick_Examples/Special_Nits.thy
changeset 63167 0909deb8059b
parent 61076 bdc1e2f0a86a
child 74641 6f801e1073fa
equal deleted inserted replaced
63166:143f58bb34f9 63167:0909deb8059b
     3     Copyright   2009-2011
     3     Copyright   2009-2011
     4 
     4 
     5 Examples featuring Nitpick's "specialize" optimization.
     5 Examples featuring Nitpick's "specialize" optimization.
     6 *)
     6 *)
     7 
     7 
     8 section {* Examples Featuring Nitpick's \textit{specialize} Optimization *}
     8 section \<open>Examples Featuring Nitpick's \textit{specialize} Optimization\<close>
     9 
     9 
    10 theory Special_Nits
    10 theory Special_Nits
    11 imports Main
    11 imports Main
    12 begin
    12 begin
    13 
    13