equal
deleted
inserted
replaced
1208 its premise. |
1208 its premise. |
1209 *} |
1209 *} |
1210 |
1210 |
1211 constdefs |
1211 constdefs |
1212 simp_implies :: "[prop, prop] => prop" (infixr "=simp=>" 1) |
1212 simp_implies :: "[prop, prop] => prop" (infixr "=simp=>" 1) |
1213 "simp_implies \<equiv> op ==>" |
1213 [code func del]: "simp_implies \<equiv> op ==>" |
1214 |
1214 |
1215 lemma simp_impliesI: |
1215 lemma simp_impliesI: |
1216 assumes PQ: "(PROP P \<Longrightarrow> PROP Q)" |
1216 assumes PQ: "(PROP P \<Longrightarrow> PROP Q)" |
1217 shows "PROP P =simp=> PROP Q" |
1217 shows "PROP P =simp=> PROP Q" |
1218 apply (unfold simp_implies_def) |
1218 apply (unfold simp_implies_def) |