doc-src/IsarImplementation/Thy/Integration.thy
Tue, 26 Oct 2010 11:22:18 +0200 wenzelm proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
less more (0) -10 -1 tip