replaced 8bit characters
authoroheimb
Mon Nov 10 14:57:31 1997 +0100 (1997-11-10)
changeset 4192c38ab5af38b5
parent 4191 f967419250d1
child 4193 a8e252c91dba
replaced 8bit characters
src/HOL/Option.thy
src/HOL/Prod.ML
src/HOL/equalities.ML
     1.1 --- a/src/HOL/Option.thy	Mon Nov 10 14:30:35 1997 +0100
     1.2 +++ b/src/HOL/Option.thy	Mon Nov 10 14:57:31 1997 +0100
     1.3 @@ -13,9 +13,9 @@
     1.4  constdefs
     1.5  
     1.6    the		:: "'a option => 'a"
     1.7 - "the  %y. case y of None => arbitrary | Some x => x"
     1.8 + "the == %y. case y of None => arbitrary | Some x => x"
     1.9  
    1.10    option_map	:: "('a => 'b) => ('a option => 'b option)"
    1.11 - "option_map  %f y. case y of None => None | Some x => Some (f x)"
    1.12 + "option_map == %f y. case y of None => None | Some x => Some (f x)"
    1.13  
    1.14  end
     2.1 --- a/src/HOL/Prod.ML	Mon Nov 10 14:30:35 1997 +0100
     2.2 +++ b/src/HOL/Prod.ML	Mon Nov 10 14:57:31 1997 +0100
     2.3 @@ -136,7 +136,7 @@
     2.4  qed "split";
     2.5  
     2.6  val split_select = prove_goalw Prod.thy [split_def] 
     2.7 -	"((x,y). P x y) = (xy. P (fst xy) (snd xy))" (K [rtac refl 1]);
     2.8 +	"(@(x,y). P x y) = (@xy. P (fst xy) (snd xy))" (K [rtac refl 1]);
     2.9  
    2.10  Addsimps [fst_conv, snd_conv, split];
    2.11  
     3.1 --- a/src/HOL/equalities.ML	Mon Nov 10 14:30:35 1997 +0100
     3.2 +++ b/src/HOL/equalities.ML	Mon Nov 10 14:57:31 1997 +0100
     3.3 @@ -369,7 +369,7 @@
     3.4  
     3.5  (*Basic identities*)
     3.6  
     3.7 -val not_empty = prove_goal Set.thy "A  {} = (x. xA)" (K [Blast_tac 1]);
     3.8 +val not_empty = prove_goal Set.thy "A ~= {} = (? x. x:A)" (K [Blast_tac 1]);
     3.9  (*Addsimps[not_empty];*)
    3.10  
    3.11  goal thy "(UN x:{}. B x) = {}";