src/HOL/Tools/ATP/remchars.pl
changeset 15658 2edb384bf61f
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/ATP/remchars.pl	Wed Apr 06 12:01:37 2005 +0200
     1.3 @@ -0,0 +1,31 @@
     1.4 +#!/usr/bin/perl
     1.5 +#
     1.6 +# isa2tex.pl - Converts isabelle formulae into LaTeX
     1.7 +# A complete hack - needs more work.
     1.8 +#
     1.9 +# by Michael Dales (michael@dcs.gla.ac.uk)
    1.10 +
    1.11 +# Begin math mode
    1.12 +#printf "\$";
    1.13 +#ALL xa::'a::type.   (~ (P::'a::type => bool) (x::'a::type) | P xa) & (~ P xa# | P x)((P::'a::type => bool) (xa::'a::type) | (ALL x::'a::type. P x)) &((AL#L x::'a::type. ~ P x) | ~ P (xb::'a::type))
    1.14 +#perhaps change to all chars not in alphanumeric or a few symbols?
    1.15 +
    1.16 +while (<STDIN>)
    1.17 +{
    1.18 +
    1.19 +    #chop();
    1.20 +    s%\n$%%;
    1.21 +    s%%%g;
    1.22 +    s%%%g;
    1.23 +    s%%%g;
    1.24 +    s%%%g;
    1.25 +    s%%%g;
    1.26 +    s%%%g;
    1.27 +    
    1.28 +    #printf "$_\\newline\n";
    1.29 +    printf "$_";
    1.30 +}
    1.31 +
    1.32 +# End math mode
    1.33 +#printf "\$\n";
    1.34 +#printf "\\end{tabbing}\n";