doc-src/IsarRef/Thy/Spec.thy
Wed, 22 Aug 2012 22:47:16 +0200 wenzelm 'ML_file' evaluates ML text from a file directly within the theory, without predeclaration via 'uses';
less more (0) -30 -10 -1 tip