equal
deleted
inserted
replaced
1146 \[ |
1146 \[ |
1147 \infer[(@{inference_def assumption})]{@{text "C\<vartheta>"}} |
1147 \infer[(@{inference_def assumption})]{@{text "C\<vartheta>"}} |
1148 {@{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> A \<^vec>x) \<Longrightarrow> C"} & @{text "A\<vartheta> = H\<^sub>i\<vartheta>"}~~\text{(for some~@{text i})}} |
1148 {@{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> A \<^vec>x) \<Longrightarrow> C"} & @{text "A\<vartheta> = H\<^sub>i\<vartheta>"}~~\text{(for some~@{text i})}} |
1149 \] |
1149 \] |
1150 |
1150 |
1151 FIXME @{inference_def elim_resolution}, @{inference_def dest_resolution} |
1151 %FIXME @{inference_def elim_resolution}, @{inference_def dest_resolution} |
1152 *} |
1152 *} |
1153 |
1153 |
1154 text %mlref {* |
1154 text %mlref {* |
1155 \begin{mldecls} |
1155 \begin{mldecls} |
1156 @{index_ML_op "RSN": "thm * (int * thm) -> thm"} \\ |
1156 @{index_ML_op "RSN": "thm * (int * thm) -> thm"} \\ |