src/Doc/Datatypes/Datatypes.thy
changeset 57984 cbe9a16f8e11
parent 57983 6edc3529bb4e
child 57988 030ff4ceb6c3
     1.1 --- a/src/Doc/Datatypes/Datatypes.thy	Mon Aug 18 17:19:58 2014 +0200
     1.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Mon Aug 18 17:20:13 2014 +0200
     1.3 @@ -831,6 +831,8 @@
     1.4  \item[@{text "t."}\hthm{split_sel_asm}\rm:] ~ \\
     1.5  @{thm list.split_sel_asm[no_vars]}
     1.6  
     1.7 +\item[@{text "t."}\hthm{split_sels} = @{text "split_sel split_sel_asm"}]
     1.8 +
     1.9  \item[@{text "t."}\hthm{case_eq_if}\rm:] ~ \\
    1.10  @{thm list.case_eq_if[no_vars]}
    1.11