src/Doc/Codegen/Further.thy
changeset 63241 f59fd6cc935e
parent 63239 d562c9948dee
child 63303 7cffe366d333
equal deleted inserted replaced
63240:f82c0b803bda 63241:f59fd6cc935e
   343 
   343 
   344   \end{description}
   344   \end{description}
   345 \<close>
   345 \<close>
   346 
   346 
   347 end
   347 end
   348