src/HOL/Predicate.thy
changeset 32235 8f9b8d14fc9f
parent 31932 685e7b450ab5
child 32372 b0d2b49bfaed
--- 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"