equal
deleted
inserted
replaced
29 |
29 |
30 "----------- the rules -------------------------------------------"; |
30 "----------- the rules -------------------------------------------"; |
31 "----------- the rules -------------------------------------------"; |
31 "----------- the rules -------------------------------------------"; |
32 "----------- the rules -------------------------------------------"; |
32 "----------- the rules -------------------------------------------"; |
33 fun str2term str = (term_of o the o (parse Biegelinie.thy)) str; |
33 fun str2term str = (term_of o the o (parse Biegelinie.thy)) str; |
34 fun term2s t = Sign.string_of_term (sign_of Biegelinie.thy) t; |
34 fun term2s t = Syntax.string_of_term (thy2ctxt' "Biegelinie") t; |
35 fun rewrit thm str = |
35 fun rewrit thm str = |
36 fst (the (rewrite_ Biegelinie.thy tless_true e_rls true thm str)); |
36 fst (the (rewrite_ Biegelinie.thy tless_true e_rls true thm str)); |
37 |
37 |
38 val t = rewrit Belastung_Querkraft (str2term "- q_ x = - q_0"); term2s t; |
38 val t = rewrit Belastung_Querkraft (str2term "- q_ x = - q_0"); term2s t; |
39 if term2s t = "Q' x = - q_0" then () |
39 if term2s t = "Q' x = - q_0" then () |