1479 "P \<or> (True \<and> Q) \<equiv> P \<or> Q"}

  1479 "P \<or> (True \<and> Q) \<equiv> P \<or> Q"}

  1480 

  1480 

  1481   The reason for this behaviour is that @{text "(op \<or>)"} expects two

  1481   The reason for this behaviour is that @{text "(op \<or>)"} expects two

  1482   arguments.  So the term must be of the form @{text "(Const \<dots> $ t1) $ t2"}. The

  1482   arguments.  So the term must be of the form @{text "(Const \<dots> $ t1) $ t2"}. The

  1483   conversion is then applied to @{text "t2"} which in the example above

  1483   conversion is then applied to @{text "t2"} which in the example above

  1485 

  1486 

  1486   The function @{ML Conv.abs_conv} applies a conversion under an abstractions.

  1487   The function @{ML Conv.abs_conv} applies a conversion under an abstractions.

  1487   For example:

  1488   For example:

  1488 

  1489 

  1489   @{ML_response_fake [display,gray]

  1490   @{ML_response_fake [display,gray]