doc-src/Intro/prod.thy
author blanchet
Fri Apr 30 09:36:45 2010 +0200 (2010-04-30)
changeset 36569 3a29eb7606c3
parent 105 216d6ed87399
permissions -rw-r--r--
added "no_atp" for theorems that are automatically used or included by Sledgehammer when appropriate (about combinators and fequal)
lcp@105
     1
Prod = FOL +
lcp@105
     2
types   "*" 2                                 (infixl 20)
lcp@105
     3
arities "*"     :: (term,term)term
lcp@105
     4
consts  fst     :: "'a * 'b => 'a"
lcp@105
     5
        snd     :: "'a * 'b => 'b"
lcp@105
     6
        Pair    :: "['a,'b] => 'a * 'b"       ("(1<_,/_>)")
lcp@105
     7
rules   fst     "fst(<a,b>) = a"
lcp@105
     8
        snd     "snd(<a,b>) = b"
lcp@105
     9
end