--- a/src/HOL/NSA/HLog.thy	Wed Dec 30 17:45:18 2015 +0100
+++ b/src/HOL/NSA/HLog.thy	Wed Dec 30 17:55:43 2015 +0100
@@ -11,10 +11,10 @@
 
 
 (* should be in NSA.ML *)
-lemma epsilon_ge_zero [simp]: "0 \<le> epsilon"
+lemma epsilon_ge_zero [simp]: "0 \<le> \<epsilon>"
 by (simp add: epsilon_def star_n_zero_num star_n_le)
 
-lemma hpfinite_witness: "epsilon : {x. 0 \<le> x & x : HFinite}"
+lemma hpfinite_witness: "\<epsilon> : {x. 0 \<le> x & x : HFinite}"
 by auto