Ignore:
Timestamp:
Nov 23, 2010, 5:44:42 PM (10 years ago)
Author:
sacerdot
Message:
  • notation moved to proper places
  • new function split on Vectors
File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/Connectives.ma

    r260 r268  
    3030ninductive Not (A:Prop): Prop ≝
    3131nmk: (A → False) → Not A.
     32
     33notation "⊥" with precedence 90
     34  for @{ match ? in False with [ ] }.
    3235
    3336interpretation "logical not" 'not x = (Not x).
Note: See TracChangeset for help on using the changeset viewer.