Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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
isabelle