equal
deleted
inserted
replaced
360 the lose de Bruijn index is replaced by a unique free variable. For example |
360 the lose de Bruijn index is replaced by a unique free variable. For example |
361 |
361 |
362 |
362 |
363 @{ML_response_fake [display,gray] |
363 @{ML_response_fake [display,gray] |
364 "let |
364 "let |
365 val app = Bound 0 $ Free (\"x\", @{typ nat}) |
365 val body = Bound 0 $ Free (\"x\", @{typ nat}) |
366 in |
366 in |
367 Term.dest_abs (\"x\", @{typ \"nat \<Rightarrow> bool\"}, app) |
367 Term.dest_abs (\"x\", @{typ \"nat \<Rightarrow> bool\"}, body) |
368 end" |
368 end" |
369 "(\"xa\", Free (\"xa\", \"nat \<Rightarrow> bool\") $ Free (\"x\", \"nat\"))"} |
369 "(\"xa\", Free (\"xa\", \"nat \<Rightarrow> bool\") $ Free (\"x\", \"nat\"))"} |
370 |
370 |
371 There are also many convenient functions that construct specific HOL-terms |
371 There are also many convenient functions that construct specific HOL-terms |
372 in the structure @{ML_struct HOLogic}. For |
372 in the structure @{ML_struct HOLogic}. For |
385 *} |
385 *} |
386 |
386 |
387 text {* |
387 text {* |
388 \begin{readmore} |
388 \begin{readmore} |
389 There are many functions in @{ML_file "Pure/term.ML"}, @{ML_file |
389 There are many functions in @{ML_file "Pure/term.ML"}, @{ML_file |
390 "Pure/logic.ML"} and @{ML_file "HOL/Tools/hologic.ML"} that make such manual |
390 "Pure/logic.ML"} and @{ML_file "HOL/Tools/hologic.ML"} that make manual |
391 constructions of terms and types easier. |
391 constructions of terms and types easier. |
392 \end{readmore} |
392 \end{readmore} |
393 |
393 |
394 When constructing terms manually, there are a few subtle issues with |
394 When constructing terms manually, there are a few subtle issues with |
395 constants. They usually crop up when pattern matching terms or types, or |
395 constants. They usually crop up when pattern matching terms or types, or |