equal
deleted
inserted
replaced
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 asm_rls = 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 = ParseC.parse_test @{context} "0 = (0::real)"; |
106 val SOME (t',_) = rewrite_ ctxt rew_ord asm_rls 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 |