# HG changeset patch # User oheimb # Date 879170251 -3600 # Node ID c38ab5af38b54794d0876cd02f71ed8f1695161f # Parent f967419250d19ab3ac0f765d1b8f20f1bbcba0b1 replaced 8bit characters diff -r f967419250d1 -r c38ab5af38b5 src/HOL/Option.thy --- 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 diff -r f967419250d1 -r c38ab5af38b5 src/HOL/Prod.ML --- 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]; diff -r f967419250d1 -r c38ab5af38b5 src/HOL/equalities.ML --- 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) = {}";