equal
deleted
inserted
replaced
222 by simp |
222 by simp |
223 |
223 |
224 |
224 |
225 subsection \<open>Initializing the fixrec package\<close> |
225 subsection \<open>Initializing the fixrec package\<close> |
226 |
226 |
227 ML_file "Tools/holcf_library.ML" |
227 ML_file \<open>Tools/holcf_library.ML\<close> |
228 ML_file "Tools/fixrec.ML" |
228 ML_file \<open>Tools/fixrec.ML\<close> |
229 |
229 |
230 method_setup fixrec_simp = \<open> |
230 method_setup fixrec_simp = \<open> |
231 Scan.succeed (SIMPLE_METHOD' o Fixrec.fixrec_simp_tac) |
231 Scan.succeed (SIMPLE_METHOD' o Fixrec.fixrec_simp_tac) |
232 \<close> "pattern prover for fixrec constants" |
232 \<close> "pattern prover for fixrec constants" |
233 |
233 |