changeset 171 | 16c4ea954511 |
parent 168 | 44ff2275d44f |
child 207 | 408713c7f66b |
--- a/IOA/meta_theory/Solve.ML Fri Nov 11 10:35:03 1994 +0100 +++ b/IOA/meta_theory/Solve.ML Mon Nov 21 17:50:34 1994 +0100 @@ -50,4 +50,4 @@ by (eres_inst_tac [("x","snd(ex,Suc(n))")] allE 1); by (eres_inst_tac [("x","a")] allE 1); by (asm_full_simp_tac SS 1); -val trace_inclusion = result(); +qed "trace_inclusion";