equal
deleted
inserted
replaced
260 |
260 |
261 subsection \<open>Further Examples\<close> |
261 subsection \<open>Further Examples\<close> |
262 |
262 |
263 text \<open> |
263 text \<open> |
264 Further examples for compiling inductive predicates can be found in |
264 Further examples for compiling inductive predicates can be found in |
265 @{file "~~/src/HOL/Predicate_Compile_Examples/Examples.thy"}. There are |
265 \<^file>\<open>~~/src/HOL/Predicate_Compile_Examples/Examples.thy\<close>. There are |
266 also some examples in the Archive of Formal Proofs, notably in the |
266 also some examples in the Archive of Formal Proofs, notably in the |
267 @{text "POPLmark-deBruijn"} and the @{text "FeatherweightJava"} |
267 @{text "POPLmark-deBruijn"} and the @{text "FeatherweightJava"} |
268 sessions. |
268 sessions. |
269 \<close> |
269 \<close> |
270 |
270 |