src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML
changeset 48325 479b4d6b9562
parent 48297 26c1a97c7784
child 48440 fce9d97a3258
     1.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML	Fri Apr 13 13:30:27 2012 +0200
     1.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML	Fri Apr 13 13:59:35 2012 +0200
     1.3 @@ -345,23 +345,23 @@
     1.4  
     1.5  fun status_to_string status_value =
     1.6    case status_value of
     1.7 -      Suc => "suc"	| Unp => "unp"
     1.8 +      Suc => "suc"  | Unp => "unp"
     1.9      | Sap => "sap"  | Esa => "esa"
    1.10      | Sat => "sat"  | Fsa => "fsa"
    1.11      | Thm => "thm"  | Wuc => "wuc"
    1.12 -    | Eqv => "eqv"	| Tac => "tac"
    1.13 -    | Wec => "wec"	| Eth => "eth"
    1.14 -    | Tau => "tau"	| Wtc => "wtc"
    1.15 -    | Wth => "wth"	| Cax => "cax"
    1.16 -    | Sca => "sca"	| Tca => "tca"
    1.17 -    | Wca => "wca"	| Cup => "cup"
    1.18 -    | Csp => "csp"	| Ecs => "ecs"
    1.19 -    | Csa => "csa"	| Cth => "cth"
    1.20 -    | Ceq => "ceq"	| Unc => "unc"
    1.21 -    | Wcc => "wcc"	| Ect => "ect"
    1.22 -    | Fun => "fun"	| Uns => "uns"
    1.23 -    | Wct => "wct"	| Scc => "scc"
    1.24 -    | Uca => "uca"	| Noc => "noc"
    1.25 +    | Eqv => "eqv"  | Tac => "tac"
    1.26 +    | Wec => "wec"  | Eth => "eth"
    1.27 +    | Tau => "tau"  | Wtc => "wtc"
    1.28 +    | Wth => "wth"  | Cax => "cax"
    1.29 +    | Sca => "sca"  | Tca => "tca"
    1.30 +    | Wca => "wca"  | Cup => "cup"
    1.31 +    | Csp => "csp"  | Ecs => "ecs"
    1.32 +    | Csa => "csa"  | Cth => "cth"
    1.33 +    | Ceq => "ceq"  | Unc => "unc"
    1.34 +    | Wcc => "wcc"  | Ect => "ect"
    1.35 +    | Fun => "fun"  | Uns => "uns"
    1.36 +    | Wct => "wct"  | Scc => "scc"
    1.37 +    | Uca => "uca"  | Noc => "noc"
    1.38  
    1.39  fun string_of_tptp_term x =
    1.40    case x of