equal
deleted
inserted
replaced
801 |
801 |
802 ML{*fun is_all (@{term All} $ _) = true |
802 ML{*fun is_all (@{term All} $ _) = true |
803 | is_all _ = false*} |
803 | is_all _ = false*} |
804 |
804 |
805 text {* |
805 text {* |
806 will not correctly match the formula @{prop "\<forall>x::nat. P x"}: |
806 will not correctly match the formula @{prop[source] "\<forall>x::nat. P x"}: |
807 |
807 |
808 @{ML_response [display,gray] "is_all @{term \"\<forall>x::nat. P x\"}" "false"} |
808 @{ML_response [display,gray] "is_all @{term \"\<forall>x::nat. P x\"}" "false"} |
809 |
809 |
810 The problem is that the @{text "@term"}-antiquotation in the pattern |
810 The problem is that the @{text "@term"}-antiquotation in the pattern |
811 fixes the type of the constant @{term "All"} to be @{typ "('a \<Rightarrow> bool) \<Rightarrow> bool"} for |
811 fixes the type of the constant @{term "All"} to be @{typ "('a \<Rightarrow> bool) \<Rightarrow> bool"} for |