equal
deleted
inserted
replaced
219 |
219 |
220 "-------- fun rules2scr_Rls --------------------------------------------------------------------"; |
220 "-------- fun rules2scr_Rls --------------------------------------------------------------------"; |
221 "-------- fun rules2scr_Rls --------------------------------------------------------------------"; |
221 "-------- fun rules2scr_Rls --------------------------------------------------------------------"; |
222 "-------- fun rules2scr_Rls --------------------------------------------------------------------"; |
222 "-------- fun rules2scr_Rls --------------------------------------------------------------------"; |
223 (*compare Prog_Expr.*) |
223 (*compare Prog_Expr.*) |
224 val prog = Auto_Prog.rules2scr_Rls @{theory} [Rule.Thm ("thm111", @{thm thm111}), Rule.Thm ("refl", @{thm refl})] |
224 val prog = Auto_Prog.rules2scr_Rls @{theory} [\<^rule_thm>\<open>thm111\<close>, \<^rule_thm>\<open>refl\<close>] |
225 ; |
225 ; |
226 writeln (UnparseC.term_in_thy @{theory} prog); |
226 writeln (UnparseC.term_in_thy @{theory} prog); |
227 (*auto_generated t_t = |
227 (*auto_generated t_t = |
228 Repeat |
228 Repeat |
229 ((Try (Repeat (Rewrite ''thm111'')) #> |
229 ((Try (Repeat (Rewrite ''thm111'')) #> |