src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML
changeset 36493 a3357a631b96
parent 36491 6769f8eacaac
child 36556 81dc2c20f052
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Wed Apr 28 15:53:17 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Wed Apr 28 16:03:49 2010 +0200
     1.3 @@ -107,13 +107,20 @@
     1.4  
     1.5  fun union_all xss = fold (union (op =)) xss []
     1.6  
     1.7 -(* Provide readable names for the more common symbolic functions *)
     1.8 +(* Readable names for the more common symbolic functions. Do not mess with the
     1.9 +   last six entries of the table unless you know what you are doing. *)
    1.10  val const_trans_table =
    1.11    Symtab.make [(@{const_name "op ="}, "equal"),
    1.12                 (@{const_name "op &"}, "and"),
    1.13                 (@{const_name "op |"}, "or"),
    1.14                 (@{const_name "op -->"}, "implies"),
    1.15 -               (@{const_name "op :"}, "in")]
    1.16 +               (@{const_name "op :"}, "in"),
    1.17 +               (@{const_name fequal}, "fequal"),
    1.18 +               (@{const_name COMBI}, "COMBI"),
    1.19 +               (@{const_name COMBK}, "COMBK"),
    1.20 +               (@{const_name COMBB}, "COMBB"),
    1.21 +               (@{const_name COMBC}, "COMBC"),
    1.22 +               (@{const_name COMBS}, "COMBS")]
    1.23  
    1.24  val type_const_trans_table =
    1.25    Symtab.make [(@{type_name "*"}, "prod"),