equal
deleted
inserted
replaced
187 |
187 |
188 declare rtranclp_eq_rtrancl_tab_nil [code_unfold, code_inline del] |
188 declare rtranclp_eq_rtrancl_tab_nil [code_unfold, code_inline del] |
189 |
189 |
190 declare rtranclp_eq_rtrancl_tab_nil[THEN iffD2, code_pred_intro] |
190 declare rtranclp_eq_rtrancl_tab_nil[THEN iffD2, code_pred_intro] |
191 |
191 |
192 code_pred rtranclp using rtranclp_eq_rtrancl_tab_nil[THEN iffD1] by fastsimp |
192 code_pred rtranclp using rtranclp_eq_rtrancl_tab_nil [THEN iffD1] by fastsimp |
193 |
193 |
194 subsection {* A simple example *} |
194 subsection {* A simple example *} |
195 |
195 |
196 datatype ty = A | B | C |
196 datatype ty = A | B | C |
197 |
197 |