src/HOL/Library/Transitive_Closure_Table.thy
changeset 45231 d85a2fdc586c
parent 45169 4baa475a51e6
child 46359 9bc43dc49d0a
     1.1 --- a/src/HOL/Library/Transitive_Closure_Table.thy	Fri Oct 21 11:17:12 2011 +0200
     1.2 +++ b/src/HOL/Library/Transitive_Closure_Table.thy	Fri Oct 21 11:17:14 2011 +0200
     1.3 @@ -185,8 +185,6 @@
     1.4      by (auto simp add: rtranclp_eq_rtrancl_path)
     1.5  qed
     1.6  
     1.7 -declare rtranclp_eq_rtrancl_tab_nil [code_unfold, code_inline del]
     1.8 -
     1.9  declare rtranclp_eq_rtrancl_tab_nil[THEN iffD2, code_pred_intro]
    1.10  
    1.11  code_pred rtranclp using rtranclp_eq_rtrancl_tab_nil [THEN iffD1] by fastforce