src/HOL/NanoJava/ROOT.ML
author schirmer
Mon, 26 Jan 2004 10:34:02 +0100
changeset 14361 ad2f5da643b4
parent 11565 ab004c0ecc63
child 33615 261abc2e3155
permissions -rw-r--r--
* Support for raw latex output in control symbols: \<^raw...> * Symbols may only start with one backslash: \<...>. \\<...> is no longer accepted by the scanner. - Adapted some Isar-theories to fit to this policy

use_thy "Example";