98 "----------- Widerspruch 3 = 777 ---------------------------------"; |
98 "----------- Widerspruch 3 = 777 ---------------------------------"; |
99 "----------- Widerspruch 3 = 777 ---------------------------------"; |
99 "----------- Widerspruch 3 = 777 ---------------------------------"; |
100 val thy = @{theory "Isac_Knowledge"}; |
100 val thy = @{theory "Isac_Knowledge"}; |
101 val ctxt = Proof_Context.init_global thy; |
101 val ctxt = Proof_Context.init_global thy; |
102 val rew_ord = Rewrite_Ord.function_empty; |
102 val rew_ord = Rewrite_Ord.function_empty; |
103 val erls = Rule_Set.Empty; |
103 val asm_rls = Rule_Set.Empty; |
104 val thm = ThmC.thm_from_thy thy "sym_mult_zero_right"; |
104 val thm = ThmC.thm_from_thy thy "sym_mult_zero_right"; |
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 asm_rls 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 (*----------------vvvvvvvvvvvvvv ERROR Unbound schematic variable: ?a1 |
110 (*----------------vvvvvvvvvvvvvv ERROR Unbound schematic variable: ?a1 |
111 --------------- review together with development of Widerspruch 3 = 77* ) |
111 --------------- review together with development of Widerspruch 3 = 77* ) |
117 val t'' = subst_atomic subst t'; |
117 val t'' = subst_atomic subst t'; |
118 UnparseC.term t'' = "0 = 3 * 0"; (* = true*) |
118 UnparseC.term t'' = "0 = 3 * 0"; (* = true*) |
119 |
119 |
120 val thm = ThmC.thm_from_thy thy "sym"; |
120 val thm = ThmC.thm_from_thy thy "sym"; |
121 (*----- STOPPED.WN0x?: Widerspruch 3 = 777: sym contains "==>" instead of "=" !!! |
121 (*----- STOPPED.WN0x?: Widerspruch 3 = 777: sym contains "==>" instead of "=" !!! |
122 val SOME (t''',_) = rewrite_ thy rew_ord erls false thm t''; |
122 val SOME (t''',_) = rewrite_ thy rew_ord asm_rls false thm t''; |
123 *) |
123 *) |
124 ( *----------------^^^^^^^^^^^^^^ ERROR Unbound schematic variable: ?a1*) |
124 ( *----------------^^^^^^^^^^^^^^ ERROR Unbound schematic variable: ?a1*) |