Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Datatype.thy
author paulson
Fri, 11 Sep 1998 16:25:40 +0200
changeset 5479 5a5dfb0f0d7d
parent 5181 4ba3787d9709
child 5714 b4f2e281a907
permissions -rw-r--r--
fixed PROOF FAILED

(*  Title:      HOL/Datatype.thy
    ID:         $Id$
    Author:     Stefan Berghofer
    Copyright   1998  TU Muenchen
*)

Datatype = Univ +

rep_datatype sum
  distinct "[[Inl_not_Inr, Inr_not_Inl]]"
  inject   "[[Inl_eq, Inr_eq]]"
  induct   sum_induct

rep_datatype prod
  distinct "[[]]"
  inject   "[[Pair_eq]]"
  induct   "allI RS (allI RS (split_paired_All RS iffD2)) RS spec"

end
isabelle