changeset 23755 | 1c4672d130b1 |
parent 23416 | b73a6b72f706 |
child 23854 | 688a8a7bcd4e |
--- a/src/HOL/Library/Graphs.thy Wed Jul 11 11:27:46 2007 +0200 +++ b/src/HOL/Library/Graphs.thy Wed Jul 11 11:28:13 2007 +0200 @@ -321,7 +321,7 @@ 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, [])"