The Theory pair
 Parents

 misc
 Children

 Constants
 IsPairRep ('a 'b BOOL) BOOL Snd ('a 'b) 'b Fst ('a 'b) 'a \$, 'a 'b 'a 'b Uncurry ('a 'b 'c) ('a 'b) 'c Curry (('a 'b) 'c) 'a 'b 'c
 Types
 '1 '2
 Fixity

 Infix 150: ,
 Terminators

 Definitions
 IsPairRep is_pair_rep_def comma mk_var("fst", (('a 'b BOOL) 'a)) mk_var("snd", (('a 'b BOOL) 'b)) ( x y IsPairRep (comma x y) mk_var("fst", (('a 'b BOOL) 'a)) (comma x y) = x mk_var("snd", (('a 'b BOOL) 'b)) (comma x y) = y) ( x y a b comma a b = comma x y a = x b = y) ( p IsPairRep p comma (mk_var("fst", (('a 'b BOOL) 'a)) p) (mk_var("snd", (('a 'b BOOL) 'b)) p) = p) _def f TypeDefn IsPairRep f , Fst Snd pair_ops_def ( x y Fst (x, y) = x Snd (x, y) = y) ( x y a b (a, b) = (x, y) a = x b = y) ( p (Fst p, Snd p) = p) Uncurry uncurry_def f x y Uncurry f (x, y) = f x y Curry curry_def f x y Curry f x y = f (x, y)
 Theorems
 pair_clauses x y a b p fu fc Fst (x, y) = x Snd (x, y) = y ((a, b) = (x, y) a = x b = y) (Fst p, Snd p) = p Curry fc x y = fc (x, y) Uncurry fu (x, y) = fu x y Uncurry fu p = fu (Fst p) (Snd p) ((a, b) = p a = Fst p b = Snd p) (p = (a, b) Fst p = a Snd p = b)