equal
deleted
inserted
replaced
205 val t = TermC.str2term |
205 val t = TermC.str2term |
206 ("[L * q_0 = c, " ^ |
206 ("[L * q_0 = c, " ^ |
207 "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, " ^ |
207 "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, " ^ |
208 "0 = c_4, " ^ |
208 "0 = c_4, " ^ |
209 "0 = c_3]"); |
209 "0 = c_3]"); |
210 val SOME (t,_) = rewrite_ ctxt e_rew_ord Rule_Set.empty false @{thm commute_0_equality} t; |
210 val SOME (t,_) = rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false @{thm commute_0_equality} t; |
211 val SOME (t,_) = rewrite_ ctxt e_rew_ord Rule_Set.empty false @{thm commute_0_equality} t; |
211 val SOME (t,_) = rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false @{thm commute_0_equality} t; |
212 val SOME (t,_) = rewrite_ ctxt e_rew_ord Rule_Set.empty false @{thm commute_0_equality} t; |
212 val SOME (t,_) = rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false @{thm commute_0_equality} t; |
213 if UnparseC.term t = |
213 if UnparseC.term t = |
214 "[L * q_0 = c, (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2 = 0,\n c_4 = 0, c_3 = 0]" |
214 "[L * q_0 = c, (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2 = 0,\n c_4 = 0, c_3 = 0]" |
215 then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 1"; |
215 then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 1"; |
216 |
216 |
217 val SOME (t,_) = rewrite_set_inst_ ctxt false subst simplify_System_parenthesized t; |
217 val SOME (t,_) = rewrite_set_inst_ ctxt false subst simplify_System_parenthesized t; |