Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
added generalize rule;
authorwenzelm
Sat, 17 Jun 2006 19:37:49 +0200
changeset 19908 f035261fb5b9
parent 19907 f552697b2f19
child 19909 6b5574d64aa4
added generalize rule;
src/Pure/proofterm.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/proofterm.ML	Sat Jun 17 19:37:48 2006 +0200
+++ b/src/Pure/proofterm.ML	Sat Jun 17 19:37:49 2006 +0200
@@ -77,6 +77,7 @@
   val freezeT : term -> proof -> proof
   val rotate_proof : term list -> term -> int -> proof -> proof
   val permute_prems_prf : term list -> int -> int -> proof -> proof
+  val generalize: string list * string list -> int -> proof -> proof
   val instantiate : ((indexname * sort) * typ) list * ((indexname * typ) * term) list
     -> proof -> proof
   val lift_proof : term -> int -> term -> proof -> proof
@@ -653,6 +654,12 @@
   end;
 
 
+(***** generalization *****)
+
+fun generalize (tfrees, frees) idx prf =
+  map_proof_terms (Term.generalize (tfrees, frees) idx) (Term.generalizeT tfrees idx) prf;
+
+
 (***** instantiation *****)
 
 fun instantiate (instT, inst) prf =
isabelle