equal
deleted
inserted
replaced
88 val terms = thms >> map Drule.dest_term; |
88 val terms = thms >> map Drule.dest_term; |
89 in |
89 in |
90 |
90 |
91 val _ = |
91 val _ = |
92 Theory.setup |
92 Theory.setup |
93 (Attrib.setup @{binding langford} |
93 (Attrib.setup \<^binding>\<open>langford\<close> |
94 ((keyword qeN |-- thms) -- |
94 ((keyword qeN |-- thms) -- |
95 (keyword gatherN |-- thms) -- |
95 (keyword gatherN |-- thms) -- |
96 (keyword atomsN |-- terms) >> (fn ((qes, gs), atoms) => |
96 (keyword atomsN |-- terms) >> (fn ((qes, gs), atoms) => |
97 if length qes = 3 andalso length gs > 1 then |
97 if length qes = 3 andalso length gs > 1 then |
98 let |
98 let |
106 "Langford data"); |
106 "Langford data"); |
107 end; |
107 end; |
108 |
108 |
109 val _ = |
109 val _ = |
110 Theory.setup |
110 Theory.setup |
111 (Attrib.setup @{binding langfordsimp} (Attrib.add_del add_simp del_simp) "Langford simpset"); |
111 (Attrib.setup \<^binding>\<open>langfordsimp\<close> (Attrib.add_del add_simp del_simp) "Langford simpset"); |
112 |
112 |
113 end; |
113 end; |