src/HOL/Library/Graphs.thy

 
 subsection {* Finite Paths *}
 
 types ('n, 'e) fpath = "('n \<times> ('e \<times> 'n) list)"
 
-inductive2  has_fpath :: "('n, 'e) graph \<Rightarrow> ('n, 'e) fpath \<Rightarrow> bool" 
+inductive  has_fpath :: "('n, 'e) graph \<Rightarrow> ('n, 'e) fpath \<Rightarrow> bool" 
   for G :: "('n, 'e) graph"
 where
   has_fpath_empty: "has_fpath G (n, [])"
 | has_fpath_join: "\<lbrakk>G \<turnstile> n \<leadsto>\<^bsup>e\<^esup> n'; has_fpath G (n', es)\<rbrakk> \<Longrightarrow> has_fpath G (n, (e, n')#es)"