src/Tools/isac/Knowledge/Equation.thy
branchisac-update-Isa09-2
changeset 38031 460c24a6a6ba
parent 38012 f57ddfd09474
child 41952 0e76e17a430a
equal deleted inserted replaced
38030:95d956108461 38031:460c24a6a6ba
    71     [((term_of o the o (parse thy)) "equality", [eq]),
    71     [((term_of o the o (parse thy)) "equality", [eq]),
    72      ((term_of o the o (parse thy)) "solveFor", [bdv]),
    72      ((term_of o the o (parse thy)) "solveFor", [bdv]),
    73      ((term_of o the o (parse thy)) "solutions", 
    73      ((term_of o the o (parse thy)) "solutions", 
    74       [(term_of o the o (parse thy)) "L"])
    74       [(term_of o the o (parse thy)) "L"])
    75      ]
    75      ]
    76   | argl2dtss _ = raise error "Equation.ML: wrong argument for argl2dtss";
    76   | argl2dtss _ = error "Equation.ML: wrong argument for argl2dtss";
    77 
    77 
    78 castab := 
    78 castab := 
    79 overwritel (!castab, 
    79 overwritel (!castab, 
    80 	    [((term_of o the o (parse thy)) "solveTest", 
    80 	    [((term_of o the o (parse thy)) "solveTest", 
    81 	      (("Test", ["univariate","equation","test"], ["no_met"]), 
    81 	      (("Test", ["univariate","equation","test"], ["no_met"]),