r226

Coq-zh · Feb 17, 2019 · 8b755f3 · 8b755f3
1 parent 8c8cec9
commit 8b755f3
Show file tree

Hide file tree

Showing 208 changed files with 288 additions and 288 deletions.
diff --git a/lf-current/Auto.html b/lf-current/Auto.html
@@ -17,7 +17,7 @@
 <div id="page">
 
 <div id="header">
-<a href='https://www.cis.upenn.edu/~bcpierce/sf/current/index.html'>
+<a href='https://coq-zh.github.io/SF-zh/index.html'>
 <img src='common/media/image/sf_logo_sm.png'></a>
 </br><a href='index.html'>  <span class='booktitleinheader'>Volume 1: 逻辑基础</span><br></br>
 <ul id='menu'>
@@ -797,7 +797,7 @@ <h1 class="libtitle">Auto<span class="subtitle">更多的自动化</span></h1>
 </div>
 <div class="code code-tight">
 
-<span class="comment">(*&nbsp;Sat&nbsp;Jan&nbsp;26&nbsp;15:14:46&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;Sun&nbsp;Feb&nbsp;17&nbsp;18:24:13&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
 </div>
 </div>
 

diff --git a/lf-current/Auto.v b/lf-current/Auto.v
@@ -601,4 +601,4 @@ Proof. eauto. Qed.
     [e] 开头的变体。 *)
 
 
-(* Sat Jan 26 15:14:46 UTC 2019 *)
+(* Sun Feb 17 18:24:13 UTC 2019 *)
diff --git a/lf-current/AutoTest.v b/lf-current/AutoTest.v
@@ -44,4 +44,4 @@ idtac "".
 idtac "********** Advanced **********".
 Abort.
 
-(* Sat Jan 26 15:15:05 UTC 2019 *)
+(* Sun Feb 17 18:24:32 UTC 2019 *)
diff --git a/lf-current/Basics.html b/lf-current/Basics.html
@@ -17,7 +17,7 @@
 <div id="page">
 
 <div id="header">
-<a href='https://www.cis.upenn.edu/~bcpierce/sf/current/index.html'>
+<a href='https://coq-zh.github.io/SF-zh/index.html'>
 <img src='common/media/image/sf_logo_sm.png'></a>
 </br><a href='index.html'>  <span class='booktitleinheader'>Volume 1: 逻辑基础</span><br></br>
 <ul id='menu'>
@@ -1673,7 +1673,7 @@ <h1 class="libtitle">Basics<span class="subtitle">Coq 函数式编程</span></h1
 <span class="proofbox">&#9744;</span> 
 <div class="code code-tight">
 
-<span class="comment">(*&nbsp;Sat&nbsp;Jan&nbsp;26&nbsp;15:14:45&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;Sun&nbsp;Feb&nbsp;17&nbsp;18:24:11&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
 </div>
 </div>
 

diff --git a/lf-current/Basics.v b/lf-current/Basics.v
@@ -1198,4 +1198,4 @@ Fixpoint bin_to_nat (m:bin) : nat
 Definition manual_grade_for_binary : option (nat*string) := None.
 (** [] *)
 
-(* Sat Jan 26 15:14:45 UTC 2019 *)
+(* Sun Feb 17 18:24:11 UTC 2019 *)
diff --git a/lf-current/BasicsTest.v b/lf-current/BasicsTest.v
@@ -192,4 +192,4 @@ idtac "".
 idtac "********** Advanced **********".
 Abort.
 
-(* Sat Jan 26 15:14:47 UTC 2019 *)
+(* Sun Feb 17 18:24:14 UTC 2019 *)
diff --git a/lf-current/Bib.html b/lf-current/Bib.html
@@ -17,7 +17,7 @@
 <div id="page">
 
 <div id="header">
-<a href='https://www.cis.upenn.edu/~bcpierce/sf/current/index.html'>
+<a href='https://coq-zh.github.io/SF-zh/index.html'>
 <img src='common/media/image/sf_logo_sm.png'></a>
 </br><a href='index.html'>  <span class='booktitleinheader'>Volume 1: 逻辑基础</span><br></br>
 <ul id='menu'>
@@ -84,7 +84,7 @@ <h1 class="libtitle">Bib<span class="subtitle">参考文献</span></h1>
 </div>
 <div class="code code-tight">
 
-<span class="comment">(*&nbsp;Sat&nbsp;Jan&nbsp;26&nbsp;15:14:46&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;Sun&nbsp;Feb&nbsp;17&nbsp;18:24:13&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
 </div>
 </div>
 

diff --git a/lf-current/Bib.v b/lf-current/Bib.v
@@ -32,4 +32,4 @@
 
 *)
 
-(* Sat Jan 26 15:14:46 UTC 2019 *)
+(* Sun Feb 17 18:24:13 UTC 2019 *)
diff --git a/lf-current/BibTest.v b/lf-current/BibTest.v
@@ -44,4 +44,4 @@ idtac "".
 idtac "********** Advanced **********".
 Abort.
 
-(* Sat Jan 26 15:15:05 UTC 2019 *)
+(* Sun Feb 17 18:24:33 UTC 2019 *)
diff --git a/lf-current/Extraction.html b/lf-current/Extraction.html
@@ -17,7 +17,7 @@
 <div id="page">
 
 <div id="header">
-<a href='https://www.cis.upenn.edu/~bcpierce/sf/current/index.html'>
+<a href='https://coq-zh.github.io/SF-zh/index.html'>
 <img src='common/media/image/sf_logo_sm.png'></a>
 </br><a href='index.html'>  <span class='booktitleinheader'>Volume 1: 逻辑基础</span><br></br>
 <ul id='menu'>
@@ -230,7 +230,7 @@ <h1 class="libtitle">Extraction<span class="subtitle">从 Coq 中提取 ML</span
 </div>
 <div class="code code-tight">
 
-<span class="comment">(*&nbsp;Sat&nbsp;Jan&nbsp;26&nbsp;15:14:46&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;Sun&nbsp;Feb&nbsp;17&nbsp;18:24:13&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
 </div>
 </div>
 

diff --git a/lf-current/Extraction.v b/lf-current/Extraction.v
@@ -116,4 +116,4 @@ Extraction "imp.ml" empty_st ceval_step parse.
 (** 有关提取的更多详情见_'软件基础'_第三卷_'已验证的函数式算法'_中的
     Extract 一章。 *)
 
-(* Sat Jan 26 15:14:46 UTC 2019 *)
+(* Sun Feb 17 18:24:13 UTC 2019 *)
diff --git a/lf-current/ExtractionTest.v b/lf-current/ExtractionTest.v
@@ -44,4 +44,4 @@ idtac "".
 idtac "********** Advanced **********".
 Abort.
 
-(* Sat Jan 26 15:15:03 UTC 2019 *)
+(* Sun Feb 17 18:24:31 UTC 2019 *)
diff --git a/lf-current/Imp.html b/lf-current/Imp.html
@@ -17,7 +17,7 @@
 <div id="page">
 
 <div id="header">
-<a href='https://www.cis.upenn.edu/~bcpierce/sf/current/index.html'>
+<a href='https://coq-zh.github.io/SF-zh/index.html'>
 <img src='common/media/image/sf_logo_sm.png'></a>
 </br><a href='index.html'>  <span class='booktitleinheader'>Volume 1: 逻辑基础</span><br></br>
 <ul id='menu'>
@@ -2550,7 +2550,7 @@ <h1 class="libtitle">Imp<span class="subtitle">简单的指令式程序</span></
 <span class="proofbox">&#9744;</span> 
 <div class="code code-tight">
 
-<span class="comment">(*&nbsp;Sat&nbsp;Jan&nbsp;26&nbsp;15:14:46&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;Sun&nbsp;Feb&nbsp;17&nbsp;18:24:13&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
 </div>
 </div>
 

diff --git a/lf-current/Imp.v b/lf-current/Imp.v
@@ -1718,4 +1718,4 @@ End BreakImp.
     [] *)
 
 
-(* Sat Jan 26 15:14:46 UTC 2019 *)
+(* Sun Feb 17 18:24:13 UTC 2019 *)
diff --git a/lf-current/ImpCEvalFun.html b/lf-current/ImpCEvalFun.html
@@ -17,7 +17,7 @@
 <div id="page">
 
 <div id="header">
-<a href='https://www.cis.upenn.edu/~bcpierce/sf/current/index.html'>
+<a href='https://coq-zh.github.io/SF-zh/index.html'>
 <img src='common/media/image/sf_logo_sm.png'></a>
 </br><a href='index.html'>  <span class='booktitleinheader'>Volume 1: 逻辑基础</span><br></br>
 <ul id='menu'>
@@ -458,7 +458,7 @@ <h1 class="libtitle">ImpCEvalFun<span class="subtitle">Imp 的求值函数</span
 </div>
 
 <br/>
-<span class="comment">(*&nbsp;Sat&nbsp;Jan&nbsp;26&nbsp;15:14:46&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;Sun&nbsp;Feb&nbsp;17&nbsp;18:24:13&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
 </div>
 </div>
 

diff --git a/lf-current/ImpCEvalFun.v b/lf-current/ImpCEvalFun.v
@@ -369,4 +369,4 @@ Proof.
   rewrite E1 in E2. inversion E2. reflexivity.
   omega. omega.  Qed.
 
-(* Sat Jan 26 15:14:46 UTC 2019 *)
+(* Sun Feb 17 18:24:13 UTC 2019 *)
diff --git a/lf-current/ImpCEvalFunTest.v b/lf-current/ImpCEvalFunTest.v
@@ -85,4 +85,4 @@ idtac "".
 idtac "********** Advanced **********".
 Abort.
 
-(* Sat Jan 26 15:15:02 UTC 2019 *)
+(* Sun Feb 17 18:24:30 UTC 2019 *)
diff --git a/lf-current/ImpParser.html b/lf-current/ImpParser.html
@@ -17,7 +17,7 @@
 <div id="page">
 
 <div id="header">
-<a href='https://www.cis.upenn.edu/~bcpierce/sf/current/index.html'>
+<a href='https://coq-zh.github.io/SF-zh/index.html'>
 <img src='common/media/image/sf_logo_sm.png'></a>
 </br><a href='index.html'>  <span class='booktitleinheader'>Volume 1: 逻辑基础</span><br></br>
 <ul id='menu'>
@@ -535,7 +535,7 @@ <h1 class="libtitle">ImpParser<span class="subtitle">用 Coq 实现词法分析
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">END</span>;;<br/>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;"x" <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> "z")%<span class="id" type="var">imp</span>.<br/>
 <span class="id" type="keyword">Proof</span>. <span class="id" type="var">cbv</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
-<span class="comment">(*&nbsp;Sat&nbsp;Jan&nbsp;26&nbsp;15:14:46&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;Sun&nbsp;Feb&nbsp;17&nbsp;18:24:13&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
 </div>
 </div>
 

diff --git a/lf-current/ImpParser.v b/lf-current/ImpParser.v
@@ -454,4 +454,4 @@ Example eg2 : parse "
       "x" ::= "z")%imp.
 Proof. cbv. reflexivity. Qed.
 
-(* Sat Jan 26 15:14:46 UTC 2019 *)
+(* Sun Feb 17 18:24:13 UTC 2019 *)
diff --git a/lf-current/ImpParserTest.v b/lf-current/ImpParserTest.v
@@ -44,4 +44,4 @@ idtac "".
 idtac "********** Advanced **********".
 Abort.
 
-(* Sat Jan 26 15:15:01 UTC 2019 *)
+(* Sun Feb 17 18:24:29 UTC 2019 *)
diff --git a/lf-current/ImpTest.v b/lf-current/ImpTest.v
@@ -246,4 +246,4 @@ idtac "---------- BreakImp.while_stops_on_break ---------".
 Print Assumptions BreakImp.while_stops_on_break.
 Abort.
 
-(* Sat Jan 26 15:15:00 UTC 2019 *)
+(* Sun Feb 17 18:24:27 UTC 2019 *)
diff --git a/lf-current/IndPrinciples.html b/lf-current/IndPrinciples.html
@@ -17,7 +17,7 @@
 <div id="page">
 
 <div id="header">
-<a href='https://www.cis.upenn.edu/~bcpierce/sf/current/index.html'>
+<a href='https://coq-zh.github.io/SF-zh/index.html'>
 <img src='common/media/image/sf_logo_sm.png'></a>
 </br><a href='index.html'>  <span class='booktitleinheader'>Volume 1: 逻辑基础</span><br></br>
 <ul id='menu'>
@@ -1015,7 +1015,7 @@ <h1 class="libtitle">IndPrinciples<span class="subtitle">归纳原理</span></h1
 </div>
 <div class="code code-tight">
 
-<span class="comment">(*&nbsp;Sat&nbsp;Jan&nbsp;26&nbsp;15:14:46&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;Sun&nbsp;Feb&nbsp;17&nbsp;18:24:12&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
 </div>
 </div>
 

diff --git a/lf-current/IndPrinciples.v b/lf-current/IndPrinciples.v
@@ -592,4 +592,4 @@ Check le_ind.
 
             因此，根据 [le_S]，[n <= S o']。  [] *)
 
-(* Sat Jan 26 15:14:46 UTC 2019 *)
+(* Sun Feb 17 18:24:12 UTC 2019 *)
diff --git a/lf-current/IndPrinciplesTest.v b/lf-current/IndPrinciplesTest.v
@@ -44,4 +44,4 @@ idtac "".
 idtac "********** Advanced **********".
 Abort.
 
-(* Sat Jan 26 15:14:57 UTC 2019 *)
+(* Sun Feb 17 18:24:24 UTC 2019 *)
diff --git a/lf-current/IndProp.html b/lf-current/IndProp.html
@@ -17,7 +17,7 @@
 <div id="page">
 
 <div id="header">
-<a href='https://www.cis.upenn.edu/~bcpierce/sf/current/index.html'>
+<a href='https://coq-zh.github.io/SF-zh/index.html'>
 <img src='common/media/image/sf_logo_sm.png'></a>
 </br><a href='index.html'>  <span class='booktitleinheader'>Volume 1: 逻辑基础</span><br></br>
 <ul id='menu'>
@@ -2789,7 +2789,7 @@ <h1 class="libtitle">IndProp<span class="subtitle">归纳定义的命题</span><
 <span class="proofbox">&#9744;</span> 
 <div class="code code-tight">
 
-<span class="comment">(*&nbsp;Sat&nbsp;Jan&nbsp;26&nbsp;15:14:46&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;Sun&nbsp;Feb&nbsp;17&nbsp;18:24:12&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
 </div>
 </div>
 

diff --git a/lf-current/IndProp.v b/lf-current/IndProp.v
@@ -1831,4 +1831,4 @@ Proof.
   (* 请在此处解答 *) Admitted.
 (** [] *)
 
-(* Sat Jan 26 15:14:46 UTC 2019 *)
+(* Sun Feb 17 18:24:12 UTC 2019 *)
diff --git a/lf-current/IndPropTest.v b/lf-current/IndPropTest.v
@@ -292,4 +292,4 @@ idtac "---------- filter_challenge ---------".
 idtac "MANUAL".
 Abort.
 
-(* Sat Jan 26 15:14:54 UTC 2019 *)
+(* Sun Feb 17 18:24:22 UTC 2019 *)
diff --git a/lf-current/Induction.html b/lf-current/Induction.html
@@ -17,7 +17,7 @@
 <div id="page">
 
 <div id="header">
-<a href='https://www.cis.upenn.edu/~bcpierce/sf/current/index.html'>
+<a href='https://coq-zh.github.io/SF-zh/index.html'>
 <img src='common/media/image/sf_logo_sm.png'></a>
 </br><a href='index.html'>  <span class='booktitleinheader'>Volume 1: 逻辑基础</span><br></br>
 <ul id='menu'>
@@ -654,7 +654,7 @@ <h1 class="libtitle">Induction<span class="subtitle">归纳证明</span></h1>
 
 
 <br/>
-<span class="comment">(*&nbsp;Sat&nbsp;Jan&nbsp;26&nbsp;15:14:45&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;Sun&nbsp;Feb&nbsp;17&nbsp;18:24:11&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
 </div>
 </div>
 

diff --git a/lf-current/Induction.v b/lf-current/Induction.v
@@ -588,4 +588,4 @@ Definition manual_grade_for_binary_inverse_c : option (nat*string) := None.
 (** [] *)
 
 
-(* Sat Jan 26 15:14:45 UTC 2019 *)
+(* Sun Feb 17 18:24:11 UTC 2019 *)
diff --git a/lf-current/InductionTest.v b/lf-current/InductionTest.v
@@ -177,4 +177,4 @@ idtac "---------- binary_inverse_c ---------".
 idtac "MANUAL".
 Abort.
 
-(* Sat Jan 26 15:14:48 UTC 2019 *)
+(* Sun Feb 17 18:24:15 UTC 2019 *)
diff --git a/lf-current/Lists.html b/lf-current/Lists.html
@@ -17,7 +17,7 @@
 <div id="page">
 
 <div id="header">
-<a href='https://www.cis.upenn.edu/~bcpierce/sf/current/index.html'>
+<a href='https://coq-zh.github.io/SF-zh/index.html'>
 <img src='common/media/image/sf_logo_sm.png'></a>
 </br><a href='index.html'>  <span class='booktitleinheader'>Volume 1: 逻辑基础</span><br></br>
 <ul id='menu'>
@@ -1480,7 +1480,7 @@ <h1 class="libtitle">Lists<span class="subtitle">使用结构化的数据</span>
 <span class="proofbox">&#9744;</span> 
 <div class="code code-tight">
 
-<span class="comment">(*&nbsp;Sat&nbsp;Jan&nbsp;26&nbsp;15:14:45&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;Sun&nbsp;Feb&nbsp;17&nbsp;18:24:11&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
 </div>
 </div>
 

diff --git a/lf-current/Lists.v b/lf-current/Lists.v
@@ -1018,4 +1018,4 @@ Inductive baz : Type :=
 Definition manual_grade_for_baz_num_elts : option (nat*string) := None.
 (** [] *)
 
-(* Sat Jan 26 15:14:45 UTC 2019 *)
+(* Sun Feb 17 18:24:11 UTC 2019 *)
diff --git a/lf-current/ListsTest.v b/lf-current/ListsTest.v
@@ -473,4 +473,4 @@ idtac "---------- rev_injective ---------".
 idtac "MANUAL".
 Abort.
 
-(* Sat Jan 26 15:14:49 UTC 2019 *)
+(* Sun Feb 17 18:24:16 UTC 2019 *)
diff --git a/lf-current/Logic.html b/lf-current/Logic.html
@@ -17,7 +17,7 @@
 <div id="page">
 
 <div id="header">
-<a href='https://www.cis.upenn.edu/~bcpierce/sf/current/index.html'>
+<a href='https://coq-zh.github.io/SF-zh/index.html'>
 <img src='common/media/image/sf_logo_sm.png'></a>
 </br><a href='index.html'>  <span class='booktitleinheader'>Volume 1: 逻辑基础</span><br></br>
 <ul id='menu'>
@@ -1948,7 +1948,7 @@ <h1 class="libtitle">Logic<span class="subtitle">Coq 中的逻辑系统</span></
 <span class="proofbox">&#9744;</span> 
 <div class="code code-tight">
 
-<span class="comment">(*&nbsp;Sat&nbsp;Jan&nbsp;26&nbsp;15:14:45&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;Sun&nbsp;Feb&nbsp;17&nbsp;18:24:12&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
 </div>
 </div>
 

diff --git a/lf-current/Logic.v b/lf-current/Logic.v
@@ -1389,4 +1389,4 @@ Definition implies_to_or := forall P Q:Prop,
 
     [] *)
 
-(* Sat Jan 26 15:14:45 UTC 2019 *)
+(* Sun Feb 17 18:24:12 UTC 2019 *)
diff --git a/lf-current/LogicTest.v b/lf-current/LogicTest.v
@@ -390,4 +390,4 @@ idtac "---------- not_exists_dist ---------".
 Print Assumptions not_exists_dist.
 Abort.
 
-(* Sat Jan 26 15:14:52 UTC 2019 *)
+(* Sun Feb 17 18:24:19 UTC 2019 *)
diff --git a/lf-current/Maps.html b/lf-current/Maps.html
@@ -17,7 +17,7 @@
 <div id="page">
 
 <div id="header">
-<a href='https://www.cis.upenn.edu/~bcpierce/sf/current/index.html'>
+<a href='https://coq-zh.github.io/SF-zh/index.html'>
 <img src='common/media/image/sf_logo_sm.png'></a>
 </br><a href='index.html'>  <span class='booktitleinheader'>Volume 1: 逻辑基础</span><br></br>
 <ul id='menu'>
@@ -526,7 +526,7 @@ <h1 class="libtitle">Maps<span class="subtitle">全映射与偏映射</span></h1
 </div>
 
 <br/>
-<span class="comment">(*&nbsp;Sat&nbsp;Jan&nbsp;26&nbsp;15:14:46&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;Sun&nbsp;Feb&nbsp;17&nbsp;18:24:12&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
 </div>
 </div>
 

diff --git a/lf-current/Maps.v b/lf-current/Maps.v
@@ -341,4 +341,4 @@ Proof.
   apply t_update_permute.
 Qed.
 
-(* Sat Jan 26 15:14:46 UTC 2019 *)
+(* Sun Feb 17 18:24:12 UTC 2019 *)
diff --git a/lf-current/MapsTest.v b/lf-current/MapsTest.v
@@ -75,4 +75,4 @@ idtac "".
 idtac "********** Advanced **********".
 Abort.
 
-(* Sat Jan 26 15:14:55 UTC 2019 *)
+(* Sun Feb 17 18:24:22 UTC 2019 *)
Original file line number	Diff line number	Diff line change
Expand Up		@@ -601,4 +601,4 @@ Proof. eauto. Qed.
		[e] 开头的变体。 *)


		(* Sat Jan 26 15:14:46 UTC 2019 *)
		(* Sun Feb 17 18:24:13 UTC 2019 *)
Original file line number	Diff line number	Diff line change
Expand Up		@@ -32,4 +32,4 @@

		*)

		(* Sat Jan 26 15:14:46 UTC 2019 *)
		(* Sun Feb 17 18:24:13 UTC 2019 *)
Original file line number	Diff line number	Diff line change
Expand Up		@@ -1718,4 +1718,4 @@ End BreakImp.
		[] *)


		(* Sat Jan 26 15:14:46 UTC 2019 *)
		(* Sun Feb 17 18:24:13 UTC 2019 *)
Original file line number	Diff line number	Diff line change
Expand Up		@@ -592,4 +592,4 @@ Check le_ind.

		因此，根据 [le_S]，[n <= S o']。 [] *)

		(* Sat Jan 26 15:14:46 UTC 2019 *)
		(* Sun Feb 17 18:24:12 UTC 2019 *)
Original file line number	Diff line number	Diff line change
Expand Up		@@ -588,4 +588,4 @@ Definition manual_grade_for_binary_inverse_c : option (nat*string) := None.
		(** [] *)


		(* Sat Jan 26 15:14:45 UTC 2019 *)
		(* Sun Feb 17 18:24:11 UTC 2019 *)
Original file line number	Diff line number	Diff line change
Expand Up		@@ -1389,4 +1389,4 @@ Definition implies_to_or := forall P Q:Prop,

		[] *)

		(* Sat Jan 26 15:14:45 UTC 2019 *)
		(* Sun Feb 17 18:24:12 UTC 2019 *)