* formal comments (text blocks etc.) in new-style theories may now
contain antiquotations of thm/prop/term/typ to be presented according
to latex print mode; concrete syntax is like this: @{term[show_types]
"f(x) = a + x"};
* Isar: theory command 'method_setup' provides a simple interface for
definining proof methods in ML;
#!/bin/sh
#
# $Id$
#
# configure - adapt Isabelle distribution to system environment
## patch scripts
if bash -c :
then
bash lib/scripts/patch-scripts.bash
else
echo "FATAL ERROR: bash not found!"
exit 2
fi