equal
deleted
inserted
replaced
1791 (ctor_set_set_inclN, map flat ctor_set_set_incl_thmsss)] @ |
1791 (ctor_set_set_inclN, map flat ctor_set_set_incl_thmsss)] @ |
1792 (if note_all then |
1792 (if note_all then |
1793 [(ctor_srelN, map single ctor_Isrel_thms)] |
1793 [(ctor_srelN, map single ctor_Isrel_thms)] |
1794 else |
1794 else |
1795 []) @ |
1795 []) @ |
1796 map2 (fn i => fn thms => (mk_ctor_setsN i, map single thms)) ls' folded_set_simp_thmss |
1796 map2 (fn i => fn thms => (mk_ctor_setN i, map single thms)) ls' folded_set_simp_thmss |
1797 |> maps (fn (thmN, thmss) => |
1797 |> maps (fn (thmN, thmss) => |
1798 map2 (fn b => fn thms => |
1798 map2 (fn b => fn thms => |
1799 ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])) |
1799 ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])) |
1800 bs thmss) |
1800 bs thmss) |
1801 in |
1801 in |