src/HOL/Relation.ML
changeset 9108 9fff97d29837
parent 9097 44cd0f9f8e5b
child 9113 e221d4f81d52
     1.1 --- a/src/HOL/Relation.ML	Thu Jun 22 11:37:13 2000 +0200
     1.2 +++ b/src/HOL/Relation.ML	Thu Jun 22 23:04:34 2000 +0200
     1.3 @@ -45,7 +45,7 @@
     1.4  by (Blast_tac 1);
     1.5  qed "diag_eqI";
     1.6  
     1.7 -val diagI = refl RS diag_eqI |> standard;
     1.8 +bind_thm ("diagI", refl RS diag_eqI |> standard);
     1.9  
    1.10  (*The general elimination rule*)
    1.11  val major::prems = Goalw [diag_def]