equal
deleted
inserted
replaced
28 val rls = assoc_rls "integration"; |
28 val rls = assoc_rls "integration"; |
29 val thy' = @{theory "Integrate"} |
29 val thy' = @{theory "Integrate"} |
30 val t = @{term "ttt :: real"}; |
30 val t = @{term "ttt :: real"}; |
31 |
31 |
32 Auto_Prog.gen thy' t rls; |
32 Auto_Prog.gen thy' t rls; |
33 "~~~~~ fun generate , args:"; val (thy, t, rls) = (thy', t, rls); |
33 "~~~~~ fun gen , args:"; val (thy, t, rls) = (thy', t, rls); |
34 val prog = case rls of |
34 val prog = case rls of |
35 Rule_Set.Repeat {rules, ...} => rules2scr_Rls thy rules |
35 Rule_Set.Repeat {rules, ...} => rules2scr_Rls thy rules |
36 | Rule_Set.Sequence {rules, ...} => rules2scr_Seq thy rules |
36 | Rule_Set.Sequence {rules, ...} => rules2scr_Seq thy rules |
37 val auto_script = subst_typs prog (type_of t) (TermC.guess_bdv_typ t) (*return from generate*); |
37 val auto_script = subst_typs prog (type_of t) (TermC.guess_bdv_typ t) (*return from generate*); |
38 |
38 |