src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
changeset 61646 61995131cf28
parent 61322 44f4ffe2b210
child 61877 276ad4354069
equal deleted inserted replaced
61645:ae5e55d03e45 61646:61995131cf28
    79 
    79 
    80 fun explode_interval _ (Facts.FromTo (i, j)) = i upto j
    80 fun explode_interval _ (Facts.FromTo (i, j)) = i upto j
    81   | explode_interval max (Facts.From i) = i upto i + max - 1
    81   | explode_interval max (Facts.From i) = i upto i + max - 1
    82   | explode_interval _ (Facts.Single i) = [i]
    82   | explode_interval _ (Facts.Single i) = [i]
    83 
    83 
    84 val backquote = raw_explode #> map (fn "`" => "\\`" | s => s) #> implode #> enclose "`" "`"
    84 val backquote = enclose "\<open>" "\<close>"
    85 
    85 
    86 (* unfolding these can yield really huge terms *)
    86 (* unfolding these can yield really huge terms *)
    87 val risky_defs = @{thms Bit0_def Bit1_def}
    87 val risky_defs = @{thms Bit0_def Bit1_def}
    88 
    88 
    89 fun is_rec_eq lhs = Term.exists_subterm (curry (op =) (head_of lhs))
    89 fun is_rec_eq lhs = Term.exists_subterm (curry (op =) (head_of lhs))