equal
deleted
inserted
replaced
63 univariate_equation_prls, SOME "solve (e_e::bool, v_v)", []))] *} |
63 univariate_equation_prls, SOME "solve (e_e::bool, v_v)", []))] *} |
64 |
64 |
65 |
65 |
66 ML{* |
66 ML{* |
67 (*.function for handling the cas-input "solve (x+1=2, x)": |
67 (*.function for handling the cas-input "solve (x+1=2, x)": |
68 make a model which is already in ptree-internal format.*) |
68 make a model which is already in ctree-internal format.*) |
69 (* val (h,argl) = strip_comb (str2term "solve (x+1=2, x)"); |
69 (* val (h,argl) = strip_comb (str2term "solve (x+1=2, x)"); |
70 val (h,argl) = strip_comb ((Thm.term_of o the o (parse thy)) |
70 val (h,argl) = strip_comb ((Thm.term_of o the o (parse thy)) |
71 "solveTest (x+1=2, x)"); |
71 "solveTest (x+1=2, x)"); |
72 *) |
72 *) |
73 fun argl2dtss [Const ("Product_Type.Pair", _) $ eq $ bdv] = |
73 fun argl2dtss [Const ("Product_Type.Pair", _) $ eq $ bdv] = |