src/Doc/Datatypes/Datatypes.thy
changeset 57494 c29729f764b1
parent 57490 afc7081f19d4
child 57526 7027cf5c1f2c
equal deleted inserted replaced
57493:554592fb795a 57494:c29729f764b1
   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