equal
deleted
inserted
replaced
2832 val ({lhs, rules = rules_idx, induct, tcs}, ctxt1) = |
2832 val ({lhs, rules = rules_idx, induct, tcs}, ctxt1) = |
2833 tfl_fn not_permissive congs wfs name R eqs ctxt; |
2833 tfl_fn not_permissive congs wfs name R eqs ctxt; |
2834 val rules = (map o map) fst (partition_eq (eq_snd (op = : int * int -> bool)) rules_idx); |
2834 val rules = (map o map) fst (partition_eq (eq_snd (op = : int * int -> bool)) rules_idx); |
2835 val simp_att = |
2835 val simp_att = |
2836 if null tcs then [Simplifier.simp_add, |
2836 if null tcs then [Simplifier.simp_add, |
2837 Named_Theorems.add @{named_theorems nitpick_simp}, Code.add_default_eqn_attribute] |
2837 Named_Theorems.add @{named_theorems nitpick_simp}, Code.add_default_eqn_attribute Code.Equation] |
2838 else []; |
2838 else []; |
2839 val ((simps' :: rules', [induct']), thy2) = |
2839 val ((simps' :: rules', [induct']), thy2) = |
2840 Proof_Context.theory_of ctxt1 |
2840 Proof_Context.theory_of ctxt1 |
2841 |> Sign.add_path bname |
2841 |> Sign.add_path bname |
2842 |> Global_Theory.add_thmss |
2842 |> Global_Theory.add_thmss |