src/HOL/Library/Transitive_Closure_Table.thy
changeset 45231 d85a2fdc586c
parent 45169 4baa475a51e6
child 46359 9bc43dc49d0a
equal deleted inserted replaced
45230:1b08942bb86f 45231:d85a2fdc586c
   183     by (rule rtrancl_tab_imp_rtrancl_path)
   183     by (rule rtrancl_tab_imp_rtrancl_path)
   184   then show "r\<^sup>*\<^sup>* x y"
   184   then show "r\<^sup>*\<^sup>* x y"
   185     by (auto simp add: rtranclp_eq_rtrancl_path)
   185     by (auto simp add: rtranclp_eq_rtrancl_path)
   186 qed
   186 qed
   187 
   187 
   188 declare rtranclp_eq_rtrancl_tab_nil [code_unfold, code_inline del]
       
   189 
       
   190 declare rtranclp_eq_rtrancl_tab_nil[THEN iffD2, code_pred_intro]
   188 declare rtranclp_eq_rtrancl_tab_nil[THEN iffD2, code_pred_intro]
   191 
   189 
   192 code_pred rtranclp using rtranclp_eq_rtrancl_tab_nil [THEN iffD1] by fastforce
   190 code_pred rtranclp using rtranclp_eq_rtrancl_tab_nil [THEN iffD1] by fastforce
   193 
   191 
   194 subsection {* A simple example *}
   192 subsection {* A simple example *}