src/HOL/Tools/ATP/remchars.pl
author paulson
Thu Apr 21 15:05:24 2005 +0200 (2005-04-21)
changeset 15789 4cb16144c81b
parent 15658 2edb384bf61f
permissions -rwxr-xr-x
added hearder lines and deleted some redundant material
quigley@15658
     1
#!/usr/bin/perl
quigley@15658
     2
#
quigley@15658
     3
# isa2tex.pl - Converts isabelle formulae into LaTeX
quigley@15658
     4
# A complete hack - needs more work.
quigley@15658
     5
#
quigley@15658
     6
# by Michael Dales (michael@dcs.gla.ac.uk)
quigley@15658
     7
quigley@15658
     8
# Begin math mode
quigley@15658
     9
#printf "\$";
quigley@15658
    10
#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))
quigley@15658
    11
#perhaps change to all chars not in alphanumeric or a few symbols?
quigley@15658
    12
quigley@15658
    13
while (<STDIN>)
quigley@15658
    14
{
quigley@15658
    15
quigley@15658
    16
    #chop();
quigley@15658
    17
    s%\n$%%;
quigley@15658
    18
    s%%%g;
quigley@15658
    19
    s%%%g;
quigley@15658
    20
    s%%%g;
quigley@15658
    21
    s%%%g;
quigley@15658
    22
    s%%%g;
quigley@15658
    23
    s%%%g;
quigley@15658
    24
    
quigley@15658
    25
    #printf "$_\\newline\n";
quigley@15658
    26
    printf "$_";
quigley@15658
    27
}
quigley@15658
    28
quigley@15658
    29
# End math mode
quigley@15658
    30
#printf "\$\n";
quigley@15658
    31
#printf "\\end{tabbing}\n";