1098   Since we want to store introduction rules associated with their 

  1098   Since we want to store introduction rules associated with their 

  1099   logical connective, we can fill the table as follows.

  1099   logical connective, we can fill the table as follows.

  1100 *}

  1100 *}

  1101 

  1101 

  1102 setup %gray {*

  1102 setup %gray {*

  1106 *}

  1106 *}

  1107 

  1107 

  1108 text {*

  1108 text {*

  1109   The use of the command \isacommand{setup} makes sure the table in the 

  1109   The use of the command \isacommand{setup} makes sure the table in the 

  1110   \emph{current} theory is updated (this is explained further in 

  1110   \emph{current} theory is updated (this is explained further in 

  1111   section~\ref{sec:theories}). The lookup can now be performed as follows.

  1111   section~\ref{sec:theories}). The lookup can now be performed as follows.

  1112 

  1112 

  1113   @{ML_response_fake [display, gray]

  1113   @{ML_response_fake [display, gray]

  1115 "SOME \"\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q\""}

  1115 "SOME \"\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q\""}

  1116 

  1116 

  1117   An important point to note is that these tables (and data in general)

  1117   An important point to note is that these tables (and data in general)

  1118   need to be treated in a purely functional fashion. Although

  1118   need to be treated in a purely functional fashion. Although

  1119   we can update the table as follows

  1119   we can update the table as follows

  1120 *}

  1120 *}

  1121 

  1121 

  1123 

  1123 

  1124 text {*

  1124 text {*

  1125   and accordingly, @{ML lookup} now produces the introduction rule for @{term "True"}

  1125   and accordingly, @{ML lookup} now produces the introduction rule for @{term "True"}

  1126   

  1126   

  1127 @{ML_response_fake [display, gray]

  1127 @{ML_response_fake [display, gray]

  1129 "SOME \"True\""}

  1129 "SOME \"True\""}

  1130 

  1130 

  1131   there are no references involved. This is one of the most fundamental

  1131   there are no references involved. This is one of the most fundamental

  1132   coding conventions for programming in Isabelle. References  

  1132   coding conventions for programming in Isabelle. References  

  1133   interfere with the multithreaded execution model of Isabelle and also

  1133   interfere with the multithreaded execution model of Isabelle and also