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.
bind_thm;
authorwenzelm
Mon, 26 Jun 2000 16:52:55 +0200
changeset 9148 4e06543e8b82
parent 9147 9a64807da023
child 9149 a126a40cba76
bind_thm;
src/HOL/Lambda/Type.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Lambda/Type.ML	Mon Jun 26 16:18:51 2000 +0200
+++ b/src/HOL/Lambda/Type.ML	Mon Jun 26 16:52:55 2000 +0200
@@ -267,7 +267,7 @@
 by (Fast_tac 1);
 qed_spec_mp "subst_Var_IT";
 
-val Var_IT = rewrite_rule [mk_meta_eq foldl_Nil] (lists.Nil RS IT.VarI);
+bind_thm ("Var_IT", rewrite_rule [mk_meta_eq foldl_Nil] (lists.Nil RS IT.VarI));
 
 Goal "t : IT ==> t $ Var i : IT";
 by (etac IT.induct 1);
isabelle