src/HOL/Fun.ML
changeset 5865 2303f5a3036d
parent 5852 4d7320490be4
child 6171 cd237a10cbf8
equal deleted inserted replaced
5864:30b6a3251813 5865:2303f5a3036d
   373 by (rename_tac "g z" 1);
   373 by (rename_tac "g z" 1);
   374 by (res_inst_tac [("x","%y. if  (y = a) then z else g y")] exI 1);
   374 by (res_inst_tac [("x","%y. if  (y = a) then z else g y")] exI 1);
   375 by (auto_tac (claset(), simpset() addsimps [split_if_mem1, split_if_eq1]));
   375 by (auto_tac (claset(), simpset() addsimps [split_if_mem1, split_if_eq1]));
   376 qed "Applyall_beta";
   376 qed "Applyall_beta";
   377 
   377 
   378 
   378 Goal "Pi {} B = { (%x. @ y. True) }";
       
   379 by (auto_tac (claset() addIs [ext], simpset() addsimps [Pi_def]));
       
   380 qed "Pi_empty";
       
   381 
       
   382 val [major] = Goalw [Pi_def] "(!!x. x: A ==> B x <= C x) ==> Pi A B <= Pi A C";
       
   383 by (auto_tac (claset(),
       
   384 	      simpset() addsimps [impOfSubs major]));
       
   385 qed "Pi_mono";