--- a/src/HOL/UNITY/Simple/Reachability.thy Wed Jul 11 11:46:05 2007 +0200
+++ b/src/HOL/UNITY/Simple/Reachability.thy Wed Jul 11 11:46:44 2007 +0200
@@ -16,15 +16,14 @@
reach :: "vertex => bool"
nmsg :: "edge => nat"
-consts REACHABLE :: "edge set"
- root :: "vertex"
+consts root :: "vertex"
E :: "edge set"
V :: "vertex set"
-inductive "REACHABLE"
- intros
- base: "v \<in> V ==> ((v,v) \<in> REACHABLE)"
- step: "((u,v) \<in> REACHABLE) & (v,w) \<in> E ==> ((u,w) \<in> REACHABLE)"
+inductive_set REACHABLE :: "edge set"
+ where
+ base: "v \<in> V ==> ((v,v) \<in> REACHABLE)"
+ | step: "((u,v) \<in> REACHABLE) & (v,w) \<in> E ==> ((u,w) \<in> REACHABLE)"
constdefs
reachable :: "vertex => state set"