src/HOLCF/IOA/meta_theory/Simulations.ML
changeset 10835 f4745d77e620
parent 10798 0a1446ff6aff
child 12218 6597093b77e7
     1.1 --- a/src/HOLCF/IOA/meta_theory/Simulations.ML	Tue Jan 09 15:32:27 2001 +0100
     1.2 +++ b/src/HOLCF/IOA/meta_theory/Simulations.ML	Tue Jan 09 15:36:30 2001 +0100
     1.3 @@ -19,7 +19,7 @@
     1.4  
     1.5  
     1.6  Goalw [Image_def]
     1.7 -"(R```{x} Int S ~= {}) = (? y. (x,y):R & y:S)";
     1.8 +"(R``{x} Int S ~= {}) = (? y. (x,y):R & y:S)";
     1.9  by (simp_tac (simpset() addsimps [Int_non_empty]) 1);
    1.10  qed"Sim_start_convert";
    1.11