src/Pure/Isar/rule_cases.ML
changeset 63512 1c7b1e294fb5
parent 61853 fb7756087101
child 67559 833d154ab189
equal deleted inserted replaced
63511:1c2c045decb3 63512:1c7b1e294fb5
    10    {fixes: (binding * typ) list,
    10    {fixes: (binding * typ) list,
    11     assumes: (string * term list) list,
    11     assumes: (string * term list) list,
    12     binds: (indexname * term option) list,
    12     binds: (indexname * term option) list,
    13     cases: (string * T) list}
    13     cases: (string * T) list}
    14   type cases = (string * T option) list
    14   type cases = (string * T option) list
       
    15   val case_conclN: string
    15   val case_hypsN: string
    16   val case_hypsN: string
       
    17   val case_premsN: string
    16   val strip_params: term -> (string * typ) list
    18   val strip_params: term -> (string * typ) list
    17   type info = ((string * string list) * string list) list
    19   type info = ((string * string list) * string list) list
    18   val make_common: Proof.context -> term -> info -> cases
    20   val make_common: Proof.context -> term -> info -> cases
    19   val make_nested: Proof.context -> term -> term -> info -> cases
    21   val make_nested: Proof.context -> term -> term -> info -> cases
    20   val apply: term list -> T -> T
    22   val apply: term list -> T -> T