src/HOL/Tools/prop_logic.ML
changeset 61332 22378817612f
parent 58322 f13f6e27d68e
child 69605 3dda49e08b9d
equal deleted inserted replaced
61331:2007ea8615a2 61332:22378817612f
   314 (* ------------------------------------------------------------------------- *)
   314 (* ------------------------------------------------------------------------- *)
   315 (* eval: given an assignment 'a' of Boolean values to variable indices, the  *)
   315 (* eval: given an assignment 'a' of Boolean values to variable indices, the  *)
   316 (*      truth value of a propositional formula 'fm' is computed              *)
   316 (*      truth value of a propositional formula 'fm' is computed              *)
   317 (* ------------------------------------------------------------------------- *)
   317 (* ------------------------------------------------------------------------- *)
   318 
   318 
   319 fun eval a True = true
   319 fun eval _ True = true
   320   | eval a False = false
   320   | eval _ False = false
   321   | eval a (BoolVar i) = (a i)
   321   | eval a (BoolVar i) = (a i)
   322   | eval a (Not fm) = not (eval a fm)
   322   | eval a (Not fm) = not (eval a fm)
   323   | eval a (Or (fm1, fm2)) = (eval a fm1) orelse (eval a fm2)
   323   | eval a (Or (fm1, fm2)) = (eval a fm1) orelse (eval a fm2)
   324   | eval a (And (fm1, fm2)) = (eval a fm1) andalso (eval a fm2);
   324   | eval a (And (fm1, fm2)) = (eval a fm1) andalso (eval a fm2);
   325 
   325