equal
deleted
inserted
replaced
105 val t = TermC.parse_test @{context} "0 = (0::real)"; |
105 val t = TermC.parse_test @{context} "0 = (0::real)"; |
106 val SOME (t',_) = rewrite_ ctxt rew_ord erls false thm t; |
106 val SOME (t',_) = rewrite_ ctxt rew_ord erls false thm t; |
107 UnparseC.term t' = "0 = ?a1 * 0"; (* = true*) |
107 UnparseC.term t' = "0 = ?a1 * 0"; (* = true*) |
108 |
108 |
109 val sube = ["?a1 = (3::real)"]; |
109 val sube = ["?a1 = (3::real)"]; |
110 val subte = Subst.input_to_terms sube; |
110 (*----------------vvvvvvvvvvvvvv ERROR Unbound schematic variable: ?a1 |
|
111 --------------- review together with development of Widerspruch 3 = 77* ) |
|
112 val subte = Subst.input_to_terms @{context} sube; |
111 UnparseC.terms_short subte = "[?a1 = 3]"; (* = true*) |
113 UnparseC.terms_short subte = "[?a1 = 3]"; (* = true*) |
112 val subst = Subst.T_from_string_eqs thy sube; |
114 val subst = Subst.T_from_string_eqs thy sube; |
113 foldl and_ (true, map TermC.contains_Var subte); |
115 foldl and_ (true, map TermC.contains_Var subte); |
114 |
116 |
115 val t'' = subst_atomic subst t'; |
117 val t'' = subst_atomic subst t'; |
117 |
119 |
118 val thm = ThmC.thm_from_thy thy "sym"; |
120 val thm = ThmC.thm_from_thy thy "sym"; |
119 (*----- STOPPED.WN0x?: Widerspruch 3 = 777: sym contains "==>" instead of "=" !!! |
121 (*----- STOPPED.WN0x?: Widerspruch 3 = 777: sym contains "==>" instead of "=" !!! |
120 val SOME (t''',_) = rewrite_ thy rew_ord erls false thm t''; |
122 val SOME (t''',_) = rewrite_ thy rew_ord erls false thm t''; |
121 *) |
123 *) |
122 |
124 ( *----------------^^^^^^^^^^^^^^ ERROR Unbound schematic variable: ?a1*) |