equal
deleted
inserted
replaced
113 Input_Descript.is_a d; (*see Input_Descript.split*) |
113 Input_Descript.is_a d; (*see Input_Descript.split*) |
114 dest_list (d,argl); |
114 dest_list (d,argl); |
115 val (_ $ v) = t; |
115 val (_ $ v) = t; |
116 TermC.is_list v; |
116 TermC.is_list v; |
117 pbl_ids ctxt d v; |
117 pbl_ids ctxt d v; |
118 [Const ("List.list.Cons", "[bool, bool List.list] => bool List.list") $ |
118 [Const (\<^const_name>\<open>Cons\<close>, "[bool, bool List.list] => bool List.list") $ |
119 (Const # $ Free # $ Const (#,#)) $ Const ("List.list.Nil", "bool List.. |
119 (Const # $ Free # $ Const (#,#)) $ Const (\<^const_name>\<open>Nil\<close>, "bool List.. |
120 |
120 |
121 val (dsc,vl) = (Input_Descript.split o Thm.term_of o the o (TermC.parse thy)) "solveFor x"; |
121 val (dsc,vl) = (Input_Descript.split o Thm.term_of o the o (TermC.parse thy)) "solveFor x"; |
122 val dsc = Const ("Input_Descript.solveFor", "RealDef.real => Tools.una") : term |
122 val dsc = Const (\<^const_name>\<open>Input_Descript.solveFor\<close>, "RealDef.real => Tools.una") : term |
123 val vl = Free ("x", "RealDef.real") : term |
123 val vl = Free ("x", "RealDef.real") : term |
124 |
124 |
125 val (dsc,id) = (split_did o Thm.term_of o the o (TermC.parse thy)) "solveFor v_"; |
125 val (dsc,id) = (split_did o Thm.term_of o the o (TermC.parse thy)) "solveFor v_"; |
126 pbl_ids ctxt dsc vl; |
126 pbl_ids ctxt dsc vl; |
127 val it = [Free ("x", "RealDef.real")] : term list |
127 val it = [Free ("x", "RealDef.real")] : term list |