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/IsarImplementation/Thy/logic.thy
changeset 20929 cd2a6d00ec47
parent 20547 796ae7fa1049
child 21324 a5089fc012b5
equal deleted inserted replaced
20928:74910a189f1d 20929:cd2a6d00ec47 
   764 *}
 
   764 *}
 
   765 
   765 
   766 
   766 
   767 section {* Rules \label{sec:rules} *}
 
   767 section {* Rules \label{sec:rules} *}
 
   768 
   768 
   769 text {*
 
   769 text %FIXME {*
 
   770 
   770 
   771 FIXME
 
   771 FIXME
 
   772 
   772 
   773   A \emph{rule} is any Pure theorem in HHF normal form; there is a
 
   773   A \emph{rule} is any Pure theorem in HHF normal form; there is a
 
   774   separate calculus for rule composition, which is modeled after
 
   774   separate calculus for rule composition, which is modeled after
isabelle