src/HOL/Induct/PropLog.thy

 
 consts
   thms  :: "'a pl set => 'a pl set"
 
 abbreviation
-  thm_rel :: "['a pl set, 'a pl] => bool"   (infixl "|-" 50)
+  thm_rel :: "['a pl set, 'a pl] => bool"   (infixl "|-" 50) where
   "H |- p == p \<in> thms H"
 
 inductive "thms(H)"
   intros
   H [intro]:  "p\<in>H ==> H |- p"

   For every valuation, if all elements of @{text H} are true then so
   is @{text p}.
 *}
 
 definition
-  sat :: "['a pl set, 'a pl] => bool"   (infixl "|=" 50)
+  sat :: "['a pl set, 'a pl] => bool"   (infixl "|=" 50) where
     "H |= p  =  (\<forall>tt. (\<forall>q\<in>H. tt[[q]]) --> tt[[p]])"
 
 
 subsection {* Proof theory of propositional logic *}