equal
deleted
inserted
replaced
529 |
529 |
530 val eqvt_thm' = |
530 val eqvt_thm' = |
531 if eqvt_flag = false then NONE |
531 if eqvt_flag = false then NONE |
532 else |
532 else |
533 let |
533 let |
534 val _ = tracing ("intrs:\n" ^ cat_lines (map @{make_string} intrs_gen)) |
534 (* val _ = tracing ("intrs:\n" ^ cat_lines (map @{make_string} intrs_gen)) *) |
535 val ([eqvt_thm], lthy) = Nominal_Eqvt.raw_equivariance false [Rdef] raw_induct intrs_gen lthy |
535 val ([eqvt_thm], lthy) = Nominal_Eqvt.raw_equivariance false [Rdef] raw_induct intrs_gen lthy |
536 in |
536 in |
537 SOME ((Nominal_ThmDecls.eqvt_transform lthy eqvt_thm) RS @{thm eqvtI}) |
537 SOME ((Nominal_ThmDecls.eqvt_transform lthy eqvt_thm) RS @{thm eqvtI}) |
538 end |
538 end |
539 |
539 |