equal
deleted
inserted
replaced
25 "-------- check auto-gen.script for Rewrite_Set_Inst -------------------------------------------"; |
25 "-------- check auto-gen.script for Rewrite_Set_Inst -------------------------------------------"; |
26 "-------- check auto-gen.script for Rewrite_Set_Inst -------------------------------------------"; |
26 "-------- check auto-gen.script for Rewrite_Set_Inst -------------------------------------------"; |
27 "-------- check auto-gen.script for Rewrite_Set_Inst -------------------------------------------"; |
27 "-------- check auto-gen.script for Rewrite_Set_Inst -------------------------------------------"; |
28 val rls = assoc_rls "integration"; |
28 val rls = assoc_rls "integration"; |
29 val thy' = @{theory "Integrate"} |
29 val thy' = @{theory "Integrate"} |
|
30 val ctxt = Proof_Context.init_global thy' |
30 val t = @{term "ttt :: real"}; |
31 val t = @{term "ttt :: real"}; |
31 |
32 |
32 Auto_Prog.gen thy' t rls; |
33 Auto_Prog.gen thy' t rls; |
33 "~~~~~ fun gen , args:"; val (thy, t, rls) = (thy', t, rls); |
34 "~~~~~ fun gen , args:"; val (thy, t, rls) = (thy', t, rls); |
34 val prog = case rls of |
35 val prog = case rls of |
51 then () else error "formal_args of auto-gen.script changed"; |
52 then () else error "formal_args of auto-gen.script changed"; |
52 |
53 |
53 Istate.init_detail (Rewrite_Set_Inst (["(''bdv'', x)"], "integration_rules")) (TermC.str2term "someTermWithBdv"); |
54 Istate.init_detail (Rewrite_Set_Inst (["(''bdv'', x)"], "integration_rules")) (TermC.str2term "someTermWithBdv"); |
54 "~~~~~ fun init_detail , args:"; val ((Tactic.Rewrite_Set_Inst (subs, rls)), t) |
55 "~~~~~ fun init_detail , args:"; val ((Tactic.Rewrite_Set_Inst (subs, rls)), t) |
55 = ((Rewrite_Set_Inst (["(''bdv'', x)"], "integration_rules")), TermC.str2term "someTermWithBdv"); |
56 = ((Rewrite_Set_Inst (["(''bdv'', x)"], "integration_rules")), TermC.str2term "someTermWithBdv"); |
56 val v = case Subst.T_from_input (ThyC.get_theory "Isac_Knowledge") subs of |
57 val v = case Subst.T_from_input ctxt subs of |
57 (_, v) :: _ => v; |
58 (_, v) :: _ => v; |
58 (*case*) assoc_rls rls (*of*); |
59 (*case*) assoc_rls rls (*of*); |
59 |
60 |
60 |
61 |
61 "-------- test the same called by interSteps norm_Poly -----------------------------------------"; |
62 "-------- test the same called by interSteps norm_Poly -----------------------------------------"; |