equal
deleted
inserted
replaced
33 |
33 |
34 val ctxt = Ctree.get_ctxt pt p; |
34 val ctxt = Ctree.get_ctxt pt p; |
35 (*must NOT check ThyC.id_empty in specify_data.spec, .. is still empty in this case |
35 (*must NOT check ThyC.id_empty in specify_data.spec, .. is still empty in this case |
36 but for References_Def.T in specify_data.origin. .. is already assigned in this case |
36 but for References_Def.T in specify_data.origin. .. is already assigned in this case |
37 and in case of CAS-cmd *) |
37 and in case of CAS-cmd *) |
38 val SOME known_x = TermC.parseNEW ctxt "x + y + z"; |
38 val known_x = TermC.parse ctxt "x + y + z"; |
39 val SOME unknown = TermC.parseNEW ctxt "a + b + c"; |
39 val unknown = TermC.parse ctxt "a + b + c"; |
40 if type_of known_x = HOLogic.realT andalso |
40 if type_of known_x = HOLogic.realT andalso |
41 type_of unknown = TFree ("'a",["Groups.plus"]) |
41 type_of unknown = TFree ("'a",["Groups.plus"]) |
42 then () else error "All_Ctx: type constraints beginning specification of root-problem "; |
42 then () else error "All_Ctx: type constraints beginning specification of root-problem "; |
43 \<close> |
43 \<close> |
44 |
44 |
72 ctxt is initialised from the thy in "SubProblem (thy, pbl, met) args" |
72 ctxt is initialised from the thy in "SubProblem (thy, pbl, met) args" |
73 and extended with the types of the variables in args.\<close> |
73 and extended with the types of the variables in args.\<close> |
74 |
74 |
75 ML \<open>(*not significant in this example*) |
75 ML \<open>(*not significant in this example*) |
76 val ctxt = Ctree.get_ctxt pt p; |
76 val ctxt = Ctree.get_ctxt pt p; |
77 val SOME known_x = TermC.parseNEW ctxt "x+y+z"; |
77 val known_x = TermC.parse ctxt "x+y+z"; |
78 val SOME unknown = TermC.parseNEW ctxt "a+b+c"; |
78 val unknown = TermC.parseparse ctxt "a+b+c"; |
79 if type_of known_x = HOLogic.realT andalso |
79 if type_of known_x = HOLogic.realT andalso |
80 type_of unknown = TFree ("'a",["Groups.plus"]) |
80 type_of unknown = TFree ("'a",["Groups.plus"]) |
81 then () else error "All_Ctx: type constraints beginning specification of SubProblem "; |
81 then () else error "All_Ctx: type constraints beginning specification of SubProblem "; |
82 \<close> |
82 \<close> |
83 |
83 |