src/Pure/Isar/element.ML
changeset 28850 6882e110c29a
parent 28832 cf7237498e7a
child 28862 53f13f763d4f
equal deleted inserted replaced
28849:9458d7a6388a 28850:6882e110c29a
    73     (Attrib.binding * (thm list * Attrib.src list) list) list ->
    73     (Attrib.binding * (thm list * Attrib.src list) list) list ->
    74     (Attrib.binding * (thm list * Attrib.src list) list) list
    74     (Attrib.binding * (thm list * Attrib.src list) list) list
    75   val generalize_facts: Proof.context -> Proof.context ->
    75   val generalize_facts: Proof.context -> Proof.context ->
    76     (Attrib.binding * (thm list * Attrib.src list) list) list ->
    76     (Attrib.binding * (thm list * Attrib.src list) list) list ->
    77     (Attrib.binding * (thm list * Attrib.src list) list) list
    77     (Attrib.binding * (thm list * Attrib.src list) list) list
    78   val activate: (Term.typ, Term.term, Facts.ref) ctxt list -> Proof.context ->
    78   val activate: (typ, term, Facts.ref) ctxt list -> Proof.context ->
    79     (context_i list * (Name.binding * Thm.thm list) list) * Proof.context
    79     (context_i list * (Name.binding * Thm.thm list) list) * Proof.context
    80   val activate_i: context_i list -> Proof.context ->
    80   val activate_i: context_i list -> Proof.context ->
    81     (context_i list * (Name.binding * Thm.thm list) list) * Proof.context
    81     (context_i list * (Name.binding * Thm.thm list) list) * Proof.context
    82 end;
    82 end;
    83 
    83