src/HOL/Trancl.ML
changeset 5608 a82a038a3e7a
parent 5479 5a5dfb0f0d7d
child 5771 7c2c8cf20221
     1.1 --- a/src/HOL/Trancl.ML	Fri Oct 02 10:44:20 1998 +0200
     1.2 +++ b/src/HOL/Trancl.ML	Fri Oct 02 14:28:39 1998 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4  
     1.5  (** The relation rtrancl **)
     1.6  
     1.7 -Goal "mono(%s. id Un (r O s))";
     1.8 +Goal "mono(%s. Id Un (r O s))";
     1.9  by (rtac monoI 1);
    1.10  by (REPEAT (ares_tac [monoI, subset_refl, comp_mono, Un_mono] 1));
    1.11  qed "rtrancl_fun_mono";
    1.12 @@ -343,6 +343,6 @@
    1.13    (K [auto_tac (claset() addEs [trancl_induct], simpset())]);
    1.14  Addsimps[trancl_empty];
    1.15  
    1.16 -qed_goal "rtrancl_empty" Trancl.thy "{}^* = id" 
    1.17 +qed_goal "rtrancl_empty" Trancl.thy "{}^* = Id" 
    1.18    (K [rtac (reflcl_trancl RS subst) 1, Simp_tac 1]);
    1.19  Addsimps[rtrancl_empty];