equal
deleted
inserted
replaced
173 There are a few naming conventions in the Isabelle code that might aid reading |
173 There are a few naming conventions in the Isabelle code that might aid reading |
174 and writing code. (Remember that code is written once, but read many |
174 and writing code. (Remember that code is written once, but read many |
175 times.) The most important conventions are: |
175 times.) The most important conventions are: |
176 |
176 |
177 \begin{itemize} |
177 \begin{itemize} |
178 \item @{text t}, @{text u} for (raw) terms; ML-type: @{ML_type term} |
178 \item @{text t}, @{text u}, @{text trm} for (raw) terms; ML-type: @{ML_type term} |
179 \item @{text ct}, @{text cu} for certified terms; ML-type: @{ML_type cterm} |
179 \item @{text ct}, @{text cu} for certified terms; ML-type: @{ML_type cterm} |
180 \item @{text "ty"}, @{text T}, @{text U} for (raw) types; ML-type: @{ML_type typ} |
180 \item @{text "ty"}, @{text T}, @{text U} for (raw) types; ML-type: @{ML_type typ} |
181 \item @{text th}, @{text thm} for theorems; ML-type: @{ML_type thm} |
181 \item @{text th}, @{text thm} for theorems; ML-type: @{ML_type thm} |
182 \item @{text "foo_tac"} for tactics; ML-type: @{ML_type tactic} |
182 \item @{text "foo_tac"} for tactics; ML-type: @{ML_type tactic} |
183 \item @{text thy} for theories; ML-type: @{ML_type theory} |
183 \item @{text thy} for theories; ML-type: @{ML_type theory} |