src/CTT/ex/Elimination.thy

--- a/src/CTT/ex/Elimination.thy	Fri Jul 15 11:26:40 2016 +0200
+++ b/src/CTT/ex/Elimination.thy	Fri Jul 15 15:19:04 2016 +0200
@@ -173,7 +173,7 @@
 apply assumption
 done
 
-text "Example of sequent_style deduction"
+text "Example of sequent-style deduction"
 (*When splitting z:A \<times> B, the assumption C(z) is affected;  ?a becomes
     \<^bold>\<lambda>u. split(u,\<lambda>v w.split(v,\<lambda>x y.\<^bold> \<lambda>z. <x,<y,z>>) ` w)     *)
 schematic_goal