--- a/ProgTutorial/Tactical.thy	Tue May 14 17:10:47 2019 +0200
+++ b/ProgTutorial/Tactical.thy	Tue May 14 17:45:13 2019 +0200
@@ -2105,9 +2105,9 @@
 in
   Thm.prop_of (Thm.beta_conversion true ctrm)
 end"
-"Const (\"Pure.eq\",\<dots>) $ 
-  (Abs (\"x\",\<dots>,Abs (\"y\",\<dots>,\<dots>)) $\<dots>$\<dots>) $ 
-    (Const (\"Groups.plus_class.plus\",\<dots>) $ \<dots> $ \<dots>)"} 
+"Const (\"Pure.eq\",_) $ 
+  (Abs (\"x\",_,Abs (\"y\",_,_)) $_$_) $ 
+    (Const (\"Groups.plus_class.plus\",_) $ _ $ _)"} 
 
 or in the pretty-printed form