equal
deleted
inserted
replaced
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)) |