doc-src/TutorialI/Rules/Forward.thy
changeset 10877 6417de2029b0
parent 10846 623141a08705
child 10958 fd582f0d649b
equal deleted inserted replaced
10876:e12892e4666a 10877:6417de2029b0
   142 
   142 
   143 
   143 
   144 lemma relprime_20_81: "gcd(#20,#81) = 1";
   144 lemma relprime_20_81: "gcd(#20,#81) = 1";
   145 by (simp add: gcd.simps)
   145 by (simp add: gcd.simps)
   146 
   146 
       
   147 text{*example of arg_cong (NEW)
       
   148 
       
   149 @{thm[display] arg_cong[no_vars]}
       
   150 \rulename{arg_cong}
       
   151 *}
   147 
   152 
   148 
   153 
   149 text {*
   154 text {*
   150 Examples of 'OF'
   155 Examples of 'OF'
   151 
   156