Deploying to gh-pages from @ ce23823 🚀

introduction.html

@@ -236,10 +236,11 @@ <h2><a class="header" href="#about-this-book" id="about-this-book">About this Bo
   have hq : q := And.right hpq
   show q ∧ p from And.intro hq hp
 </code></pre>
-<p>If you are reading the book inside of <a href="https://code.visualstudio.com/">VS Code</a>, you will see a button that reads &quot;try it!&quot; Pressing the button copies the example to your editor with enough surrounding context to make the code compile correctly. You can type
-things into the editor and modify the examples, and Lean will check the results and provide feedback continuously as you
-type. We recommend running the examples and experimenting with the code on your own as you work through the chapters
-that follow. You can open this book on VS Code by using the command &quot;Lean 4: Open Documentation View&quot;.</p>
+<p>Next to every code example in this book, you will see a button that reads &quot;Copy to clipboard&quot;. 
+Pressing the button copies the example with enough surrounding context to make the code compile correctly.
+You can paste the example code into <a href="https://code.visualstudio.com/">VS Code</a> and modify the examples, and Lean will check the results and provide feedback continuously as you type. 
+We recommend running the examples and experimenting with the code on your own as you work through the chapters that follow. 
+You can open this book in VS Code by using the command &quot;Lean 4: Docs: Show Documentation Resources&quot; and selecting &quot;Theorem Proving in Lean 4&quot; in the tab that opens.</p>
 <h2><a class="header" href="#acknowledgments" id="acknowledgments">Acknowledgments</a></h2>
 <p>This tutorial is an open access project maintained on Github. Many people have contributed to the effort, providing
 corrections, suggestions, examples, and text. We are grateful to Ulrik Buchholz, Kevin Buzzard, Mario Carneiro, Nathan

print.html

@@ -245,10 +245,11 @@ <h2><a class="header" href="#about-this-book" id="about-this-book">About this Bo
   have hq : q := And.right hpq
   show q ∧ p from And.intro hq hp
 </code></pre>
-<p>If you are reading the book inside of <a href="https://code.visualstudio.com/">VS Code</a>, you will see a button that reads &quot;try it!&quot; Pressing the button copies the example to your editor with enough surrounding context to make the code compile correctly. You can type
-things into the editor and modify the examples, and Lean will check the results and provide feedback continuously as you
-type. We recommend running the examples and experimenting with the code on your own as you work through the chapters
-that follow. You can open this book on VS Code by using the command &quot;Lean 4: Open Documentation View&quot;.</p>
+<p>Next to every code example in this book, you will see a button that reads &quot;Copy to clipboard&quot;. 
+Pressing the button copies the example with enough surrounding context to make the code compile correctly.
+You can paste the example code into <a href="https://code.visualstudio.com/">VS Code</a> and modify the examples, and Lean will check the results and provide feedback continuously as you type. 
+We recommend running the examples and experimenting with the code on your own as you work through the chapters that follow. 
+You can open this book in VS Code by using the command &quot;Lean 4: Docs: Show Documentation Resources&quot; and selecting &quot;Theorem Proving in Lean 4&quot; in the tab that opens.</p>
 <h2><a class="header" href="#acknowledgments" id="acknowledgments">Acknowledgments</a></h2>
 <p>This tutorial is an open access project maintained on Github. Many people have contributed to the effort, providing
 corrections, suggestions, examples, and text. We are grateful to Ulrik Buchholz, Kevin Buzzard, Mario Carneiro, Nathan