replaced 8bit characters
authoroheimb
Mon, 10 Nov 1997 14:57:31 +0100
changeset 4192 c38ab5af38b5
parent 4191 f967419250d1
child 4193 a8e252c91dba
replaced 8bit characters
src/HOL/Option.thy
src/HOL/Prod.ML
src/HOL/equalities.ML
--- 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. xA)" (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) = {}";