Mercurial > cpdt > repo

comparison src/DeBruijn.v @ 302:7b38729be069

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Tweak mark-up to support coqdoc 8.3
author Adam Chlipala <adam@chlipala.net>
date Mon, 17 Jan 2011 15:12:30 -0500
parents da9ccc6bf572
children d5787b70cf48
comparison
equal deleted inserted replaced
301:f4768d5a75eb 302:7b38729be069
316 Each iteration of the loop ends by calling [simp] again, and, after no more progress can be made, we finish by calling [eauto]. 316 Each iteration of the loop ends by calling [simp] again, and, after no more progress can be made, we finish by calling [eauto].
317 317
318 [[ 318 [[
319 end; simp); eauto. 319 end; simp); eauto.
320 320
321 ]] *) 321 ]]
322 *)
322 323
323 324
324 (** * Theorems *) 325 (** * Theorems *)
325 326
326 (** We are now ready to prove our main theorem, by way of a progression of lemmas. 327 (** We are now ready to prove our main theorem, by way of a progression of lemmas.