--- a/src/HOL/Hyperreal/NatStar.ML Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Hyperreal/NatStar.ML Tue Jan 09 15:32:27 2001 +0100
@@ -117,7 +117,7 @@
simpset()));
qed "NatStar_mem";
-Goalw [starsetNat_def] "hypnat_of_nat `` A <= *sNat* A";
+Goalw [starsetNat_def] "hypnat_of_nat ` A <= *sNat* A";
by (auto_tac (claset(), simpset() addsimps [hypnat_of_nat_def]));
by (blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 1);
qed "NatStar_hypreal_of_real_image_subset";
@@ -128,7 +128,7 @@
qed "NatStar_SHNat_subset";
Goalw [starsetNat_def]
- "*sNat* X Int SNat = hypnat_of_nat `` X";
+ "*sNat* X Int SNat = hypnat_of_nat ` X";
by (auto_tac (claset(),
simpset() addsimps
[hypnat_of_nat_def,SHNat_def]));
@@ -140,7 +140,7 @@
by (Auto_tac);
qed "NatStar_hypreal_of_real_Int";
-Goal "x ~: hypnat_of_nat `` A ==> ALL y: A. x ~= hypnat_of_nat y";
+Goal "x ~: hypnat_of_nat ` A ==> ALL y: A. x ~= hypnat_of_nat y";
by (Auto_tac);
qed "lemma_not_hypnatA";
@@ -188,15 +188,15 @@
qed "starfunNat2_n_starfunNat2";
Goalw [congruent_def]
- "congruent hypnatrel (%X. hypnatrel```{%n. f (X n)})";
+ "congruent hypnatrel (%X. hypnatrel``{%n. f (X n)})";
by (safe_tac (claset()));
by (ALLGOALS(Fuf_tac));
qed "starfunNat_congruent";
(* f::nat=>real *)
Goalw [starfunNat_def]
- "(*fNat* f) (Abs_hypnat(hypnatrel```{%n. X n})) = \
-\ Abs_hypreal(hyprel ``` {%n. f (X n)})";
+ "(*fNat* f) (Abs_hypnat(hypnatrel``{%n. X n})) = \
+\ Abs_hypreal(hyprel `` {%n. f (X n)})";
by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
by (simp_tac (simpset() addsimps
[hyprel_in_hypreal RS Abs_hypreal_inverse]) 1);
@@ -205,8 +205,8 @@
(* f::nat=>nat *)
Goalw [starfunNat2_def]
- "(*fNat2* f) (Abs_hypnat(hypnatrel```{%n. X n})) = \
-\ Abs_hypnat(hypnatrel ``` {%n. f (X n)})";
+ "(*fNat2* f) (Abs_hypnat(hypnatrel``{%n. X n})) = \
+\ Abs_hypnat(hypnatrel `` {%n. f (X n)})";
by (res_inst_tac [("f","Abs_hypnat")] arg_cong 1);
by (simp_tac (simpset() addsimps
[hypnatrel_in_hypnat RS Abs_hypnat_inverse,
@@ -413,14 +413,14 @@
Internal functions - some redundancy with *fNat* now
---------------------------------------------------------*)
Goalw [congruent_def]
- "congruent hypnatrel (%X. hypnatrel```{%n. f n (X n)})";
+ "congruent hypnatrel (%X. hypnatrel``{%n. f n (X n)})";
by (safe_tac (claset()));
by (ALLGOALS(Fuf_tac));
qed "starfunNat_n_congruent";
Goalw [starfunNat_n_def]
- "(*fNatn* f) (Abs_hypnat(hypnatrel```{%n. X n})) = \
-\ Abs_hypreal(hyprel ``` {%n. f n (X n)})";
+ "(*fNatn* f) (Abs_hypnat(hypnatrel``{%n. X n})) = \
+\ Abs_hypreal(hyprel `` {%n. f n (X n)})";
by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
by Auto_tac;
by (Ultra_tac 1);
@@ -468,7 +468,7 @@
by (auto_tac (claset(), simpset() addsimps [starfunNat_n, hypreal_minus]));
qed "starfunNat_n_minus";
-Goal "(*fNatn* f) (hypnat_of_nat n) = Abs_hypreal(hyprel ``` {%i. f i n})";
+Goal "(*fNatn* f) (hypnat_of_nat n) = Abs_hypreal(hyprel `` {%i. f i n})";
by (auto_tac (claset(), simpset() addsimps [starfunNat_n,hypnat_of_nat_def]));
qed "starfunNat_n_eq";
Addsimps [starfunNat_n_eq];