equal
deleted
inserted
replaced
182 |
182 |
183 \begin{readmore} |
183 \begin{readmore} |
184 The standard inductive package is based on least fix-points. It allows more |
184 The standard inductive package is based on least fix-points. It allows more |
185 general introduction rules that can include any monotone operators and also |
185 general introduction rules that can include any monotone operators and also |
186 provides a richer reasoning infrastructure. The code of this package can be found in |
186 provides a richer reasoning infrastructure. The code of this package can be found in |
187 @{ML_file "HOL/Tools/inductive_package.ML"}. |
187 @{ML_file "HOL/Tools/inductive.ML"}. |
188 \end{readmore} |
188 \end{readmore} |
189 *} |
189 *} |
190 |
190 |
191 section {* Definitional Packages *} |
191 section {* Definitional Packages *} |
192 |
192 |
193 text {* Type declarations *} |
193 text {* Type declarations *} |
194 |
194 |
195 ML{*TypedefPackage.add_typedef false NONE (@{binding test},[],NoSyn) |
195 ML{*Typedef.add_typedef false NONE (@{binding test},[],NoSyn) |
196 @{term "{1}::nat set"} NONE (simp_tac @{simpset} 1) @{theory} *} |
196 @{term "{1}::nat set"} NONE (simp_tac @{simpset} 1) @{theory} *} |
197 |
197 |
198 |
198 |
199 (*<*)end(*>*) |
199 (*<*)end(*>*) |