equal
deleted
inserted
replaced
1468 "@{ctyp \"nat \<Rightarrow> bool\"}" |
1468 "@{ctyp \"nat \<Rightarrow> bool\"}" |
1469 "nat \<Rightarrow> bool"} |
1469 "nat \<Rightarrow> bool"} |
1470 |
1470 |
1471 Since certified terms are, unlike terms, abstract objects, we cannot |
1471 Since certified terms are, unlike terms, abstract objects, we cannot |
1472 pattern-match against them. However, we can construct them. For example |
1472 pattern-match against them. However, we can construct them. For example |
1473 the function @{ML_ind capply in Thm} produces a certified application. |
1473 the function @{ML_ind apply in Thm} produces a certified application. |
1474 |
1474 |
1475 @{ML_response_fake [display,gray] |
1475 @{ML_response_fake [display,gray] |
1476 "Thm.capply @{cterm \"P::nat \<Rightarrow> bool\"} @{cterm \"3::nat\"}" |
1476 "Thm.apply @{cterm \"P::nat \<Rightarrow> bool\"} @{cterm \"3::nat\"}" |
1477 "P 3"} |
1477 "P 3"} |
1478 |
1478 |
1479 Similarly the function @{ML_ind list_comb in Drule} from the structure @{ML_struct Drule} |
1479 Similarly the function @{ML_ind list_comb in Drule} from the structure @{ML_struct Drule} |
1480 applies a list of @{ML_type cterm}s. |
1480 applies a list of @{ML_type cterm}s. |
1481 |
1481 |