doc-src/Main/Docs/Main_Doc.thy
changeset 40272 b12ae2445985
parent 38767 d8da44a8dd25
child 41532 0d34deffb0e9
equal deleted inserted replaced
40271:6014e8252e57 40272:b12ae2445985
   499 @{const List.lenlex} & @{term_type_only List.lenlex "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\
   499 @{const List.lenlex} & @{term_type_only List.lenlex "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\
   500 @{const List.lex} & @{term_type_only List.lex "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\
   500 @{const List.lex} & @{term_type_only List.lex "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\
   501 @{const List.lexn} & @{term_type_only List.lexn "('a*'a)set\<Rightarrow>nat\<Rightarrow>('a list * 'a list)set"}\\
   501 @{const List.lexn} & @{term_type_only List.lexn "('a*'a)set\<Rightarrow>nat\<Rightarrow>('a list * 'a list)set"}\\
   502 @{const List.lexord} & @{term_type_only List.lexord "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\
   502 @{const List.lexord} & @{term_type_only List.lexord "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\
   503 @{const List.listrel} & @{term_type_only List.listrel "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\
   503 @{const List.listrel} & @{term_type_only List.listrel "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\
       
   504 @{const List.listrel1} & @{term_type_only List.listrel1 "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\
   504 @{const List.lists} & @{term_type_only List.lists "'a set\<Rightarrow>'a list set"}\\
   505 @{const List.lists} & @{term_type_only List.lists "'a set\<Rightarrow>'a list set"}\\
   505 @{const List.listset} & @{term_type_only List.listset "'a set list \<Rightarrow> 'a list set"}\\
   506 @{const List.listset} & @{term_type_only List.listset "'a set list \<Rightarrow> 'a list set"}\\
   506 @{const List.listsum} & @{typeof List.listsum}\\
   507 @{const List.listsum} & @{typeof List.listsum}\\
   507 @{const List.list_all2} & @{typeof List.list_all2}\\
   508 @{const List.list_all2} & @{typeof List.list_all2}\\
   508 @{const List.list_update} & @{typeof List.list_update}\\
   509 @{const List.list_update} & @{typeof List.list_update}\\