equal
deleted
inserted
replaced
32 "----------- problemtype --------------------------------"; |
32 "----------- problemtype --------------------------------"; |
33 val pbt = {Given =["functionTerm f_f", "differentiateFor v_v"], |
33 val pbt = {Given =["functionTerm f_f", "differentiateFor v_v"], |
34 Where =[], |
34 Where =[], |
35 Find =["derivative f_f'"], |
35 Find =["derivative f_f'"], |
36 With =[], |
36 With =[], |
37 Relate=[]}:string ppc; |
37 Relate=[]}:string model; |
38 val chkpbt = ((map (TermC.parseNEW' ctxt)) o P_Model.to_list) pbt; |
38 val chkpbt = ((map (TermC.parseNEW' ctxt)) o P_Model.to_list) pbt; |
39 |
39 |
40 val org = ["functionTerm (d_d x (x \<up> 2 + 3 * x + 4))", |
40 val org = ["functionTerm (d_d x (x \<up> 2 + 3 * x + 4))", |
41 "differentiateFor x", "derivative f_f'"]; |
41 "differentiateFor x", "derivative f_f'"]; |
42 val chkorg = map (TermC.parseNEW' ctxt) org; |
42 val chkorg = map (TermC.parseNEW' ctxt) org; |
46 |
46 |
47 "----------- for correction of diff_const ---------------"; |
47 "----------- for correction of diff_const ---------------"; |
48 "----------- for correction of diff_const ---------------"; |
48 "----------- for correction of diff_const ---------------"; |
49 "----------- for correction of diff_const ---------------"; |
49 "----------- for correction of diff_const ---------------"; |
50 val ctxt = Proof_Context.init_global @{theory}; |
50 val ctxt = Proof_Context.init_global @{theory}; |
51 (*re-evaluate this file, otherwise > *** ME_Isa: 'erls' not known*) |
51 (*re-evaluate this file, otherwise > *** ME_Isa: 'asm_rls' not known*) |
52 val t = TermC.parseNEW' ctxt "Not (x =!= a)"; |
52 val t = TermC.parseNEW' ctxt "Not (x =!= a)"; |
53 case rewrite_set_ ctxt false erls_diff t of |
53 case rewrite_set_ ctxt false erls_diff t of |
54 SOME (Const (\<^const_name>\<open>True\<close>, _), []) => () |
54 SOME (Const (\<^const_name>\<open>True\<close>, _), []) => () |
55 | _ => error "rewrite_set_ Not (x =!= a) changed"; |
55 | _ => error "rewrite_set_ Not (x =!= a) changed"; |
56 |
56 |