equal
deleted
inserted
replaced
1073 \end{itemize} |
1073 \end{itemize} |
1074 *} |
1074 *} |
1075 |
1075 |
1076 text %mlref {* |
1076 text %mlref {* |
1077 \begin{mldecls} |
1077 \begin{mldecls} |
1078 @{index_ML Simplifier.norm_hhf: "thm -> thm"} \\ |
1078 @{index_ML Simplifier.norm_hhf: "Proof.context -> thm -> thm"} \\ |
1079 \end{mldecls} |
1079 \end{mldecls} |
1080 |
1080 |
1081 \begin{description} |
1081 \begin{description} |
1082 |
1082 |
1083 \item @{ML Simplifier.norm_hhf}~@{text thm} normalizes the given |
1083 \item @{ML Simplifier.norm_hhf}~@{text "ctxt thm"} normalizes the given |
1084 theorem according to the canonical form specified above. This is |
1084 theorem according to the canonical form specified above. This is |
1085 occasionally helpful to repair some low-level tools that do not |
1085 occasionally helpful to repair some low-level tools that do not |
1086 handle Hereditary Harrop Formulae properly. |
1086 handle Hereditary Harrop Formulae properly. |
1087 |
1087 |
1088 \end{description} |
1088 \end{description} |