doc-src/IsarImplementation/Thy/logic.thy
changeset 26872 336dfd860744
parent 24972 acafb18a47dc
child 28017 4919bd124a58
equal deleted inserted replaced
26871:996add9defab 26872:336dfd860744
   435   plain natural deduction rules for the primary connectives @{text
   435   plain natural deduction rules for the primary connectives @{text
   436   "\<And>"} and @{text "\<Longrightarrow>"} of the framework.  There is also a builtin
   436   "\<And>"} and @{text "\<Longrightarrow>"} of the framework.  There is also a builtin
   437   notion of equality/equivalence @{text "\<equiv>"}.
   437   notion of equality/equivalence @{text "\<equiv>"}.
   438 *}
   438 *}
   439 
   439 
   440 subsection {* Primitive connectives and rules \label{sec:prim_rules} *}
   440 subsection {* Primitive connectives and rules \label{sec:prim-rules} *}
   441 
   441 
   442 text {*
   442 text {*
   443   The theory @{text "Pure"} contains constant declarations for the
   443   The theory @{text "Pure"} contains constant declarations for the
   444   primitive connectives @{text "\<And>"}, @{text "\<Longrightarrow>"}, and @{text "\<equiv>"} of
   444   primitive connectives @{text "\<And>"}, @{text "\<Longrightarrow>"}, and @{text "\<equiv>"} of
   445   the logical framework, see \figref{fig:pure-connectives}.  The
   445   the logical framework, see \figref{fig:pure-connectives}.  The