81 val thy = @{theory "Test"}; |
81 val thy = @{theory "Test"}; |
82 val fmz = ["realTestGiven (((1+2)*4/3) \<up> 2)", "realTestFind s"]; |
82 val fmz = ["realTestGiven (((1+2)*4/3) \<up> 2)", "realTestFind s"]; |
83 val (dI',pI',mI') = |
83 val (dI',pI',mI') = |
84 ("Test", ["calculate", "test"], ["Test", "test_calculate"]); |
84 ("Test", ["calculate", "test"], ["Test", "test_calculate"]); |
85 |
85 |
86 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
86 val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))]; |
87 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
87 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
88 (*nxt =("Add_Given",Add_Given "realTestGiven (((#1 + #2) * #4 // #3) \<up> #2)")*) |
88 (*nxt =("Add_Given",Add_Given "realTestGiven (((#1 + #2) * #4 // #3) \<up> #2)")*) |
89 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
89 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
90 (*nxt = ("Add_Find",Add_Find "realTestFind s") : string * tac*) |
90 (*nxt = ("Add_Find",Add_Find "realTestFind s") : string * tac*) |
91 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
91 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |