making the evaluation of HOL.implies lazy even in strict languages by mapping it to an if statement
authorbulwahn
Wed Apr 20 07:44:23 2011 +0200 (2011-04-20)
changeset 424208a09dfeb2cec
parent 42419 9c81298fa4e1
child 42421 6bc725d60593
making the evaluation of HOL.implies lazy even in strict languages by mapping it to an if statement
src/HOL/HOL.thy
     1.1 --- a/src/HOL/HOL.thy	Tue Apr 19 14:52:22 2011 +0200
     1.2 +++ b/src/HOL/HOL.thy	Wed Apr 20 07:44:23 2011 +0200
     1.3 @@ -1915,18 +1915,22 @@
     1.4    (Haskell "Bool")
     1.5    (Scala "Boolean")
     1.6  
     1.7 -code_const True and False and Not and HOL.conj and HOL.disj and If
     1.8 +code_const True and False and Not and HOL.conj and HOL.disj and HOL.implies and If 
     1.9    (SML "true" and "false" and "not"
    1.10      and infixl 1 "andalso" and infixl 0 "orelse"
    1.11 +    and "!(if (_)/ then (_)/ else true)"
    1.12      and "!(if (_)/ then (_)/ else (_))")
    1.13    (OCaml "true" and "false" and "not"
    1.14      and infixl 3 "&&" and infixl 2 "||"
    1.15 +    and "!(if (_)/ then (_)/ else true)"
    1.16      and "!(if (_)/ then (_)/ else (_))")
    1.17    (Haskell "True" and "False" and "not"
    1.18      and infixr 3 "&&" and infixr 2 "||"
    1.19 +    and "!(if (_)/ then (_)/ else True)"
    1.20      and "!(if (_)/ then (_)/ else (_))")
    1.21    (Scala "true" and "false" and "'! _"
    1.22      and infixl 3 "&&" and infixl 1 "||"
    1.23 +    and "!(if ((_))/ (_)/ else true)"
    1.24      and "!(if ((_))/ (_)/ else (_))")
    1.25  
    1.26  code_reserved SML