equal
deleted
inserted
replaced
101 end; |
101 end; |
102 |
102 |
103 |
103 |
104 (* filter_name *) |
104 (* filter_name *) |
105 |
105 |
106 fun match_string pat str = |
|
107 let |
|
108 fun match [] _ = true |
|
109 | match (p :: ps) s = |
|
110 size p <= size s andalso |
|
111 (case try (unprefix p) s of |
|
112 SOME s' => match ps s' |
|
113 | NONE => match (p :: ps) (String.substring (s, 1, size s - 1))); |
|
114 in match (space_explode "*" pat) str end; |
|
115 |
|
116 fun filter_name str_pat (thmref, _) = |
106 fun filter_name str_pat (thmref, _) = |
117 if match_string str_pat (Facts.name_of_ref thmref) |
107 if match_string str_pat (Facts.name_of_ref thmref) |
118 then SOME (0, 0) else NONE; |
108 then SOME (0, 0) else NONE; |
119 |
|
120 |
109 |
121 (* filter intro/elim/dest/solves rules *) |
110 (* filter intro/elim/dest/solves rules *) |
122 |
111 |
123 fun filter_dest ctxt goal (_, thm) = |
112 fun filter_dest ctxt goal (_, thm) = |
124 let |
113 let |