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