--- a/src/HOL/Predicate.thy Mon Jul 27 17:36:30 2009 +0200
+++ b/src/HOL/Predicate.thy Mon Jul 27 21:47:41 2009 +0200
@@ -221,11 +221,11 @@
subsubsection {* Composition *}
inductive
- pred_comp :: "['b => 'c => bool, 'a => 'b => bool] => 'a => 'c => bool"
+ pred_comp :: "['a => 'b => bool, 'b => 'c => bool] => 'a => 'c => bool"
(infixr "OO" 75)
- for r :: "'b => 'c => bool" and s :: "'a => 'b => bool"
+ for r :: "'a => 'b => bool" and s :: "'b => 'c => bool"
where
- pred_compI [intro]: "s a b ==> r b c ==> (r OO s) a c"
+ pred_compI [intro]: "r a b ==> s b c ==> (r OO s) a c"
inductive_cases pred_compE [elim!]: "(r OO s) a c"