src/Doc/Isar_Ref/Quick_Reference.thy
changeset 62268 3d86222b4a94
parent 61656 cfabbc083977
child 62270 77e3ffb5aeb3
--- a/src/Doc/Isar_Ref/Quick_Reference.thy	Sat Feb 06 19:26:02 2016 +0100
+++ b/src/Doc/Isar_Ref/Quick_Reference.thy	Sun Feb 07 14:36:16 2016 +0100
@@ -57,13 +57,9 @@
       @{command "proof"}~\<open>m\<^sub>1\<close>~@{command "qed"}~\<open>m\<^sub>2\<close> \\
     @{command ".."} & \<open>\<equiv>\<close> & @{command "by"}~\<open>standard\<close> \\
     @{command "."} & \<open>\<equiv>\<close> & @{command "by"}~\<open>this\<close> \\
-    @{command "hence"} & \<open>\<equiv>\<close> & @{command "then"}~@{command "have"} \\
-    @{command "thus"} & \<open>\<equiv>\<close> & @{command "then"}~@{command "show"} \\
     @{command "from"}~\<open>a\<close> & \<open>\<equiv>\<close> & @{command "note"}~\<open>a\<close>~@{command "then"} \\
     @{command "with"}~\<open>a\<close> & \<open>\<equiv>\<close> & @{command "from"}~\<open>a \<AND> this\<close> \\
     @{command "from"}~\<open>this\<close> & \<open>\<equiv>\<close> & @{command "then"} \\
-    @{command "from"}~\<open>this\<close>~@{command "have"} & \<open>\<equiv>\<close> & @{command "hence"} \\
-    @{command "from"}~\<open>this\<close>~@{command "show"} & \<open>\<equiv>\<close> & @{command "thus"} \\
   \end{tabular}
 \<close>