--- a/src/HOL/Option.thy Mon Nov 10 14:30:35 1997 +0100
+++ b/src/HOL/Option.thy Mon Nov 10 14:57:31 1997 +0100
@@ -13,9 +13,9 @@
constdefs
the :: "'a option => 'a"
- "the Ú %y. case y of None => arbitrary | Some x => x"
+ "the == %y. case y of None => arbitrary | Some x => x"
option_map :: "('a => 'b) => ('a option => 'b option)"
- "option_map Ú %f y. case y of None => None | Some x => Some (f x)"
+ "option_map == %f y. case y of None => None | Some x => Some (f x)"
end
--- a/src/HOL/Prod.ML Mon Nov 10 14:30:35 1997 +0100
+++ b/src/HOL/Prod.ML Mon Nov 10 14:57:31 1997 +0100
@@ -136,7 +136,7 @@
qed "split";
val split_select = prove_goalw Prod.thy [split_def]
- "(®(x,y). P x y) = (®xy. P (fst xy) (snd xy))" (K [rtac refl 1]);
+ "(@(x,y). P x y) = (@xy. P (fst xy) (snd xy))" (K [rtac refl 1]);
Addsimps [fst_conv, snd_conv, split];
--- a/src/HOL/equalities.ML Mon Nov 10 14:30:35 1997 +0100
+++ b/src/HOL/equalities.ML Mon Nov 10 14:57:31 1997 +0100
@@ -369,7 +369,7 @@
(*Basic identities*)
-val not_empty = prove_goal Set.thy "A Û {} = (Ãx. xÎA)" (K [Blast_tac 1]);
+val not_empty = prove_goal Set.thy "A ~= {} = (? x. x:A)" (K [Blast_tac 1]);
(*Addsimps[not_empty];*)
goal thy "(UN x:{}. B x) = {}";