equal
deleted
inserted
replaced
933 |
933 |
934 ML{*fun is_all (@{term All} $ _) = true |
934 ML{*fun is_all (@{term All} $ _) = true |
935 | is_all _ = false*} |
935 | is_all _ = false*} |
936 |
936 |
937 text {* |
937 text {* |
938 will not correctly match the formula @{prop "\<forall>x::nat. P x"}: |
938 will not correctly match the formula @{prop[source] "\<forall>x::nat. P x"}: |
939 |
939 |
940 @{ML_response [display,gray] "is_all @{term \"\<forall>x::nat. P x\"}" "false"} |
940 @{ML_response [display,gray] "is_all @{term \"\<forall>x::nat. P x\"}" "false"} |
941 |
941 |
942 The problem is that the @{text "@term"}-antiquotation in the pattern |
942 The problem is that the @{text "@term"}-antiquotation in the pattern |
943 fixes the type of the constant @{term "All"} to be @{typ "('a \<Rightarrow> bool) \<Rightarrow> bool"} for |
943 fixes the type of the constant @{term "All"} to be @{typ "('a \<Rightarrow> bool) \<Rightarrow> bool"} for |