src/HOL/Inverse_Image.ML

--- a/src/HOL/Inverse_Image.ML	Tue Jan 09 15:18:07 2001 +0100
+++ b/src/HOL/Inverse_Image.ML	Tue Jan 09 15:22:13 2001 +0100
@@ -8,32 +8,32 @@
 
 (** Basic rules **)
 
-Goalw [vimage_def] "(a : f-``B) = (f a : B)";
+Goalw [vimage_def] "(a : f-`B) = (f a : B)";
 by (Blast_tac 1) ;
 qed "vimage_eq";
 
 Addsimps [vimage_eq];
 
-Goal "(a : f-``{b}) = (f a = b)";
+Goal "(a : f-`{b}) = (f a = b)";
 by (simp_tac (simpset() addsimps [vimage_eq]) 1) ;
 qed "vimage_singleton_eq";
 
 Goalw [vimage_def]
-    "!!A B f. [| f a = b;  b:B |] ==> a : f-``B";
+    "!!A B f. [| f a = b;  b:B |] ==> a : f-`B";
 by (Blast_tac 1) ;
 qed "vimageI";
 
-Goalw [vimage_def] "f a : A ==> a : f -`` A";
+Goalw [vimage_def] "f a : A ==> a : f -` A";
 by (Fast_tac 1);
 qed "vimageI2";
 
 val major::prems = Goalw [vimage_def]
-    "[| a: f-``B;  !!x.[| f a = x;  x:B |] ==> P |] ==> P";
+    "[| a: f-`B;  !!x.[| f a = x;  x:B |] ==> P |] ==> P";
 by (rtac (major RS CollectE) 1);
 by (blast_tac (claset() addIs prems) 1) ;
 qed "vimageE";
 
-Goalw [vimage_def] "a : f -`` A ==> f a : A";
+Goalw [vimage_def] "a : f -` A ==> f a : A";
 by (Fast_tac 1);
 qed "vimageD";
 
@@ -43,66 +43,66 @@
 
 (*** Equations ***)
 
-Goal "f-``{} = {}";
+Goal "f-`{} = {}";
 by (Blast_tac 1);
 qed "vimage_empty";
 
-Goal "f-``(-A) = -(f-``A)";
+Goal "f-`(-A) = -(f-`A)";
 by (Blast_tac 1);
 qed "vimage_Compl";
 
-Goal "f-``(A Un B) = (f-``A) Un (f-``B)";
+Goal "f-`(A Un B) = (f-`A) Un (f-`B)";
 by (Blast_tac 1);
 qed "vimage_Un";
 
-Goal "f -`` (A Int B) = (f -`` A) Int (f -`` B)";
+Goal "f -` (A Int B) = (f -` A) Int (f -` B)";
 by (Fast_tac 1);
 qed "vimage_Int";
 
-Goal "f -`` (Union A) = (UN X:A. f -`` X)";
+Goal "f -` (Union A) = (UN X:A. f -` X)";
 by (Blast_tac 1);
 qed "vimage_Union";
 
-Goal "f-``(UN x:A. B x) = (UN x:A. f -`` B x)";
+Goal "f-`(UN x:A. B x) = (UN x:A. f -` B x)";
 by (Blast_tac 1);
 qed "vimage_UN";
 
-Goal "f-``(INT x:A. B x) = (INT x:A. f -`` B x)";
+Goal "f-`(INT x:A. B x) = (INT x:A. f -` B x)";
 by (Blast_tac 1);
 qed "vimage_INT";
 
-Goal "f -`` Collect P = {y. P (f y)}";
+Goal "f -` Collect P = {y. P (f y)}";
 by (Blast_tac 1);
 qed "vimage_Collect_eq";
 Addsimps [vimage_Collect_eq];
 
 (*A strange result used in Tools/inductive_package*)
-val prems = Goal "(!!x. P (f x) = Q x) ==> f -`` (Collect P) = Collect Q";
+val prems = Goal "(!!x. P (f x) = Q x) ==> f -` (Collect P) = Collect Q";
 by (force_tac (claset(), simpset() addsimps prems) 1);
 qed "vimage_Collect";
 
 Addsimps [vimage_empty, vimage_Un, vimage_Int];
 
 (*NOT suitable for rewriting because of the recurrence of {a}*)
-Goal "f-``(insert a B) = (f-``{a}) Un (f-``B)";
+Goal "f-`(insert a B) = (f-`{a}) Un (f-`B)";
 by (Blast_tac 1);
 qed "vimage_insert";
 
-Goal "f-``(A-B) = (f-``A) - (f-``B)";
+Goal "f-`(A-B) = (f-`A) - (f-`B)";
 by (Blast_tac 1);
 qed "vimage_Diff";
 
-Goal "f-``UNIV = UNIV";
+Goal "f-`UNIV = UNIV";
 by (Blast_tac 1);
 qed "vimage_UNIV";
 Addsimps [vimage_UNIV];
 
 (*NOT suitable for rewriting*)
-Goal "f-``B = (UN y: B. f-``{y})";
+Goal "f-`B = (UN y: B. f-`{y})";
 by (Blast_tac 1);
 qed "vimage_eq_UN";
 
 (*monotonicity*)
-Goal "A<=B ==> f-``A <= f-``B";
+Goal "A<=B ==> f-`A <= f-`B";
 by (Blast_tac 1);
 qed "vimage_mono";