equal
deleted
inserted
replaced
874 @{thm list.sel_map[no_vars]} |
874 @{thm list.sel_map[no_vars]} |
875 |
875 |
876 \item[@{text "t."}\hthm{rel\_inject} @{text "[simp]"}\rm:] ~ \\ |
876 \item[@{text "t."}\hthm{rel\_inject} @{text "[simp]"}\rm:] ~ \\ |
877 @{thm list.rel_inject(1)[no_vars]} \\ |
877 @{thm list.rel_inject(1)[no_vars]} \\ |
878 @{thm list.rel_inject(2)[no_vars]} |
878 @{thm list.rel_inject(2)[no_vars]} |
|
879 |
|
880 \item[@{text "t."}\hthm{rel\_intros}\rm:] ~ \\ |
|
881 @{thm list.rel_intros(1)[no_vars]} \\ |
|
882 @{thm list.rel_intros(2)[no_vars]} |
879 |
883 |
880 \item[@{text "t."}\hthm{rel\_distinct} @{text "[simp]"}\rm:] ~ \\ |
884 \item[@{text "t."}\hthm{rel\_distinct} @{text "[simp]"}\rm:] ~ \\ |
881 @{thm list.rel_distinct(1)[no_vars]} \\ |
885 @{thm list.rel_distinct(1)[no_vars]} \\ |
882 @{thm list.rel_distinct(2)[no_vars]} |
886 @{thm list.rel_distinct(2)[no_vars]} |
883 |
887 |