TFL/tfl.sig
changeset 3333 0bbf06e86c06
parent 3302 404fe31fd8d2
child 3391 5e45dd3b64e9
equal deleted inserted replaced
3332:3921ebbd9cf0 3333:0bbf06e86c06
    18 
    18 
    19    val mk_functional : theory -> term
    19    val mk_functional : theory -> term
    20                        -> {functional:term,
    20                        -> {functional:term,
    21                            pats: pattern list}
    21                            pats: pattern list}
    22 
    22 
    23    val wfrec_definition0 : theory -> term -> term -> thm * theory
    23    val wfrec_definition0 : theory -> string -> term -> term -> thm * theory
    24 
    24 
    25    val post_definition : theory * (thm * pattern list)
    25    val post_definition : theory * (thm * pattern list)
    26                               -> {theory : theory,
    26                               -> {theory : theory,
    27                                   rules  : thm, 
    27                                   rules  : thm, 
    28                                     TCs  : term list list,
    28                                     TCs  : term list list,