equal
deleted
inserted
replaced
76 "3.2.2. x = 0 + 1\n" ^ |
76 "3.2.2. x = 0 + 1\n" ^ |
77 (*([3,2,2], Res), x = 1) only by Test_Tool.show_pt_tac*) |
77 (*([3,2,2], Res), x = 1) only by Test_Tool.show_pt_tac*) |
78 "4. [x = 1]\n" |
78 "4. [x = 1]\n" |
79 (*". [x = 1]" only by Test_Tool.show_pt_tac*) |
79 (*". [x = 1]" only by Test_Tool.show_pt_tac*) |
80 then () else error "intermediate steps CHANGED"; |
80 then () else error "intermediate steps CHANGED"; |
|
81 |
|
82 (*ctxt*)Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*) |