equal
deleted
inserted
replaced
16 |
16 |
17 |
17 |
18 "-------- fun eval_leaf -------------------------------------------------------------------"; |
18 "-------- fun eval_leaf -------------------------------------------------------------------"; |
19 "-------- fun eval_leaf -------------------------------------------------------------------"; |
19 "-------- fun eval_leaf -------------------------------------------------------------------"; |
20 "-------- fun eval_leaf -------------------------------------------------------------------"; |
20 "-------- fun eval_leaf -------------------------------------------------------------------"; |
21 val {scr = Prog sc, ...} = get_met ["Test","sqrt-equ-test"]; |
21 val {scr = Prog sc, ...} = Method.from_store ["Test","sqrt-equ-test"]; |
22 case eval_leaf [] NONE TermC.empty sc of |
22 case eval_leaf [] NONE TermC.empty sc of |
23 (Expr (Const ("HOL.eq", _) $ |
23 (Expr (Const ("HOL.eq", _) $ |
24 (Const ("Test.solve_root_equ", _) $ Free ("e_e", _) $ Free ("v_v", _)) $ |
24 (Const ("Test.solve_root_equ", _) $ Free ("e_e", _) $ Free ("v_v", _)) $ |
25 (Const ("HOL.Let", _) $ |
25 (Const ("HOL.Let", _) $ |
26 (Const ("Tactical.Chain", _) $ |
26 (Const ("Tactical.Chain", _) $ |