renamed UNION_... to UN_..., INTER_... to INT_... (to fit the convention)
authorpaulson
Thu, 17 Jun 1999 10:36:03 +0200
changeset 6834 44da4a2a9ef3
parent 6833 15d6c121d75f
child 6835 588f791ee737
renamed UNION_... to UN_..., INTER_... to INT_... (to fit the convention)
src/HOL/UNITY/Extend.ML
--- a/src/HOL/UNITY/Extend.ML	Thu Jun 17 10:35:01 1999 +0200
+++ b/src/HOL/UNITY/Extend.ML	Thu Jun 17 10:36:03 1999 +0200
@@ -66,7 +66,7 @@
 Goalw [extend_set_def]
     "extend_set h (INTER A B) = (INT x:A. extend_set h (B x))";
 by (force_tac (claset() addIs  [h_f_g_eq RS sym], simpset()) 1);
-qed "extend_set_INTER_distrib";
+qed "extend_set_INT_distrib";
 
 Goalw [extend_set_def]
     "extend_set h (A - B) = extend_set h A - extend_set h B";
@@ -178,8 +178,8 @@
 
 Goal "extend h (JOIN I F) = (JN i:I. extend h (F i))";
 by (rtac program_equalityI 1);
-by (simp_tac (simpset() addsimps [image_UNION, Acts_JN]) 2);
-by (simp_tac (simpset() addsimps [extend_set_INTER_distrib]) 1);
+by (simp_tac (simpset() addsimps [image_UN, Acts_JN]) 2);
+by (simp_tac (simpset() addsimps [extend_set_INT_distrib]) 1);
 qed "extend_JN";
 Addsimps [extend_JN];