src/HOL/Fun.ML
changeset 9108 9fff97d29837
parent 8767 eae30939b592
child 9339 0d8b0eb2932d
     1.1 --- a/src/HOL/Fun.ML	Thu Jun 22 11:37:13 2000 +0200
     1.2 +++ b/src/HOL/Fun.ML	Thu Jun 22 23:04:34 2000 +0200
     1.3 @@ -151,7 +151,7 @@
     1.4      "(!! x y. [| f(x) = f(y);  x:A;  y:A |] ==> x=y) ==> inj_on f A";
     1.5  by (blast_tac (claset() addIs prems) 1);
     1.6  qed "inj_onI";
     1.7 -val injI = inj_onI;                  (*for compatibility*)
     1.8 +bind_thm ("injI", inj_onI);                  (*for compatibility*)
     1.9  
    1.10  val [major] = Goal 
    1.11      "(!!x. x:A ==> g(f(x)) = x) ==> inj_on f A";
    1.12 @@ -159,7 +159,7 @@
    1.13  by (etac (apply_inverse RS trans) 1);
    1.14  by (REPEAT (eresolve_tac [asm_rl,major] 1));
    1.15  qed "inj_on_inverseI";
    1.16 -val inj_inverseI = inj_on_inverseI;   (*for compatibility*)
    1.17 +bind_thm ("inj_inverseI", inj_on_inverseI);   (*for compatibility*)
    1.18  
    1.19  Goal "(inj f) = (inv f o f = id)";
    1.20  by (asm_simp_tac (simpset() addsimps [o_def, expand_fun_eq]) 1);
    1.21 @@ -483,7 +483,7 @@
    1.22  Goalw [Pi_def] "[| f: Pi A B; g: Pi A B; ! x: A. f x = g x |] ==> f = g";
    1.23  by (rtac ext 1);
    1.24  by Auto_tac;
    1.25 -val Pi_extensionality = ballI RSN (3, result());
    1.26 +bind_thm ("Pi_extensionality", ballI RSN (3, result()));
    1.27  
    1.28  
    1.29  (*** compose ***)