| author | Walther Neuper <neuper@ist.tugraz.at> |
| Thu, 12 Aug 2010 15:03:34 +0200 | |
| branch | isac-from-Isabelle2009-2 |
| changeset 37913 | 20e3616b2d9c |
| parent 105 | 216d6ed87399 |
| permissions | -rw-r--r-- |
| 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 |