Mercurial > cpdt > repo

comparison src/Universes.v @ 554:93471096cdd4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Merge
author Adam Chlipala <adam@chlipala.net>
date Sat, 19 Aug 2017 12:14:40 -0400
parents 2c8c693ddaba
children af97676583f3
comparison
equal deleted inserted replaced
553:cb81f74d8c92 554:93471096cdd4
1066 proof p 1066 proof p
1067 ]] 1067 ]]
1068 1068
1069 The first goal looks reasonable. Hypothesis [H0] is clearly contradictory, as [discriminate] can show. *) 1069 The first goal looks reasonable. Hypothesis [H0] is clearly contradictory, as [discriminate] can show. *)
1070 1070
1071 discriminate. 1071 try discriminate. (* Note: Coq 8.6 is now solving this subgoal automatically!
1072 * This line left here to keep everything working in
1073 * 8.4, 8.5, and 8.6. *)
1072 (** %\vspace{-.15in}%[[ 1074 (** %\vspace{-.15in}%[[
1073 H : proof p 1075 H : proof p
1074 H1 : And p q = And p0 q0 1076 H1 : And p q = And p0 q0
1075 ============================ 1077 ============================
1076 proof p0 1078 proof p0