--- a/src/HOL/Induct/Exp.ML Fri Jan 05 18:33:47 2001 +0100
+++ b/src/HOL/Induct/Exp.ML Fri Jan 05 18:48:18 2001 +0100
@@ -84,14 +84,14 @@
(*Expression evaluation is functional, or deterministic*)
-Goalw [univalent_def] "univalent eval";
+Goalw [single_valued_def] "single_valued eval";
by (EVERY1[rtac allI, rtac allI, rtac impI]);
by (split_all_tac 1);
by (etac eval_induct 1);
by (dtac com_Unique 4);
by (ALLGOALS Full_simp_tac);
by (ALLGOALS Blast_tac);
-qed "univalent_eval";
+qed "single_valued_eval";
Goal "(e,s) -|-> (v,s') ==> (e = N n) --> (v=n & s'=s)";