equal
deleted
inserted
replaced
103 fun repeat_sep s f = f ::: Scan.repeat (str s |-- f) |
103 fun repeat_sep s f = f ::: Scan.repeat (str s |-- f) |
104 |
104 |
105 val parse_id = Scan.one Symbol.is_letter ::: Scan.many Symbol.is_letdig >> implode |
105 val parse_id = Scan.one Symbol.is_letter ::: Scan.many Symbol.is_letdig >> implode |
106 |
106 |
107 fun parse_varpow ctxt = parse_id -- Scan.optional (str "^" |-- nat) 1 >> |
107 fun parse_varpow ctxt = parse_id -- Scan.optional (str "^" |-- nat) 1 >> |
108 (fn (x, k) => (Thm.cterm_of ctxt (Free (x, @{typ real})), k)) |
108 (fn (x, k) => (Thm.cterm_of ctxt (Free (x, \<^typ>\<open>real\<close>)), k)) |
109 |
109 |
110 fun parse_monomial ctxt = repeat_sep "*" (parse_varpow ctxt) >> |
110 fun parse_monomial ctxt = repeat_sep "*" (parse_varpow ctxt) >> |
111 (fn xs => fold FuncUtil.Ctermfunc.update xs FuncUtil.Ctermfunc.empty) |
111 (fn xs => fold FuncUtil.Ctermfunc.update xs FuncUtil.Ctermfunc.empty) |
112 |
112 |
113 fun parse_cmonomial ctxt = |
113 fun parse_cmonomial ctxt = |