src/HOL/Tools/datatype_aux.ML
changeset 18349 58de95a16d3c
parent 18319 c52b139ebde0
child 18377 0e1d025d57b3
equal deleted inserted replaced
18348:b5d7649f8aca 18349:58de95a16d3c
    13   val foldl1 : ('a * 'a -> 'a) -> 'a list -> 'a
    13   val foldl1 : ('a * 'a -> 'a) -> 'a list -> 'a
    14 
    14 
    15   val add_path : bool -> string -> theory -> theory
    15   val add_path : bool -> string -> theory -> theory
    16   val parent_path : bool -> theory -> theory
    16   val parent_path : bool -> theory -> theory
    17 
    17 
       
    18   val store_thmss_atts : string -> string list -> theory attribute list list -> thm list list
       
    19     -> theory -> thm list list * theory
    18   val store_thmss : string -> string list -> thm list list -> theory -> thm list list * theory
    20   val store_thmss : string -> string list -> thm list list -> theory -> thm list list * theory
    19   val store_thms_atts : string -> string list -> theory attribute list list -> thm list
    21   val store_thms_atts : string -> string list -> theory attribute list list -> thm list
    20     -> theory -> thm list * theory
    22     -> theory -> thm list * theory
    21   val store_thms : string -> string list -> thm list -> theory -> thm list * theory
    23   val store_thms : string -> string list -> thm list -> theory -> thm list * theory
    22 
    24