src/HOL/Set.ML
changeset 4830 bd73675adbed
parent 4770 3e026ace28da
child 5069 3ea049f7979d
     1.1 --- a/src/HOL/Set.ML	Mon Apr 27 13:47:46 1998 +0200
     1.2 +++ b/src/HOL/Set.ML	Mon Apr 27 16:45:11 1998 +0200
     1.3 @@ -643,19 +643,19 @@
     1.4  
     1.5  
     1.6  (** Rewrite rules for boolean case-splitting: faster than 
     1.7 -	addsplits[expand_if]
     1.8 +	addsplits[split_if]
     1.9  **)
    1.10  
    1.11 -bind_thm ("expand_if_eq1", read_instantiate [("P", "%x. x = ?b")] expand_if);
    1.12 -bind_thm ("expand_if_eq2", read_instantiate [("P", "%x. ?a = x")] expand_if);
    1.13 +bind_thm ("split_if_eq1", read_instantiate [("P", "%x. x = ?b")] split_if);
    1.14 +bind_thm ("split_if_eq2", read_instantiate [("P", "%x. ?a = x")] split_if);
    1.15  
    1.16 -bind_thm ("expand_if_mem1", 
    1.17 -    read_instantiate_sg (sign_of Set.thy) [("P", "%x. x : ?b")] expand_if);
    1.18 -bind_thm ("expand_if_mem2", 
    1.19 -    read_instantiate_sg (sign_of Set.thy) [("P", "%x. ?a : x")] expand_if);
    1.20 +bind_thm ("split_if_mem1", 
    1.21 +    read_instantiate_sg (sign_of Set.thy) [("P", "%x. x : ?b")] split_if);
    1.22 +bind_thm ("split_if_mem2", 
    1.23 +    read_instantiate_sg (sign_of Set.thy) [("P", "%x. ?a : x")] split_if);
    1.24  
    1.25 -val expand_ifs = [if_bool_eq_conj, expand_if_eq1, expand_if_eq2,
    1.26 -		  expand_if_mem1, expand_if_mem2];
    1.27 +val split_ifs = [if_bool_eq_conj, split_if_eq1, split_if_eq2,
    1.28 +		  split_if_mem1, split_if_mem2];
    1.29  
    1.30  
    1.31  (*Each of these has ALREADY been added to simpset() above.*)