doc-src/IsarImplementation/Thy/logic.thy
 changeset 20929 cd2a6d00ec47 parent 20547 796ae7fa1049 child 21324 a5089fc012b5
equal 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