150 if Rule_Set.id rls = HOLogic.dest_string rls_ then |
150 if Rule_Set.id rls = HOLogic.dest_string rls_ then |
151 if f = f_ then |
151 if f = f_ then |
152 Associated (m, f', ContextC.insert_assumptions asms' ctxt) |
152 Associated (m, f', ContextC.insert_assumptions asms' ctxt) |
153 else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt) |
153 else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt) |
154 else Not_Associated |
154 else Not_Associated |
155 | associate _ ctxt (m as Tactic.Detail_Set_Inst' (_, _, _, rls, f, (f', asms')), |
|
156 (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ f_)) = |
|
157 if Rule_Set.id rls = HOLogic.dest_string rls_ then |
|
158 if f = f_ then |
|
159 Associated (m, f', ContextC.insert_assumptions asms' ctxt) |
|
160 else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt) |
|
161 else Not_Associated |
|
162 | associate _ ctxt (m as Tactic.Rewrite_Set' (_, _, rls, f, (f', asms')), |
155 | associate _ ctxt (m as Tactic.Rewrite_Set' (_, _, rls, f, (f', asms')), |
163 (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_)) = |
|
164 if Rule_Set.id rls = HOLogic.dest_string rls_ then |
|
165 if f = f_ then |
|
166 Associated (m, f', ContextC.insert_assumptions asms' ctxt) |
|
167 else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt) |
|
168 else Not_Associated |
|
169 | associate _ ctxt (m as Tactic.Detail_Set' (_, _, rls, f, (f', asms')), |
|
170 (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_)) = |
156 (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_)) = |
171 if Rule_Set.id rls = HOLogic.dest_string rls_ then |
157 if Rule_Set.id rls = HOLogic.dest_string rls_ then |
172 if f = f_ then |
158 if f = f_ then |
173 Associated (m, f', ContextC.insert_assumptions asms' ctxt) |
159 Associated (m, f', ContextC.insert_assumptions asms' ctxt) |
174 else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt) |
160 else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt) |