doc-src/IsarRef/Thy/Outer_Syntax.thy
Sun, 31 Oct 2010 13:26:37 +0100 wenzelm syntax category "real" subsumes plain "int";
less more (0) -10 -1 tip