src/HOL/UNITY/Lift.ML
changeset 6614 2d47dee036b5
parent 6570 a7d7985050a9
child 6676 62d1e642da30
equal deleted inserted replaced
6613:250a0ca35ef5 6614:2d47dee036b5
     7 *)
     7 *)
     8 
     8 
     9 (*split_all_tac causes a big blow-up*)
     9 (*split_all_tac causes a big blow-up*)
    10 claset_ref() := claset() delSWrapper record_split_name;
    10 claset_ref() := claset() delSWrapper record_split_name;
    11 
    11 
    12 Delsimps [split_paired_All];
       
    13 
       
    14 Goal "[| x ~: A;  y : A |] ==> x ~= y";
    12 Goal "[| x ~: A;  y : A |] ==> x ~= y";
    15 by (Blast_tac 1);
    13 by (Blast_tac 1);
    16 qed "not_mem_distinct";
    14 qed "not_mem_distinct";
    17 
    15 
    18 fun distinct_tac i =
    16 fun distinct_tac i =
    53 
    51 
    54 Addsimps (map simp_of_set always_defs);
    52 Addsimps (map simp_of_set always_defs);
    55 
    53 
    56 
    54 
    57 val LeadsTo_Trans_Un' = rotate_prems 1 LeadsTo_Trans_Un;
    55 val LeadsTo_Trans_Un' = rotate_prems 1 LeadsTo_Trans_Un;
    58 (* [| Lprg : B LeadsTo C; Lprg : A LeadsTo B |] ==> Lprg : (A Un B) LeadsTo C *)
    56 (* [| Lprg: B LeadsTo C; Lprg: A LeadsTo B |] ==> Lprg: (A Un B) LeadsTo C *)
    59 
    57 
    60 
    58 
    61 (*Simplification for records*)
    59 (*Simplification for records*)
    62 Addsimps (thms"state.update_defs");
    60 Addsimps (thms"state.update_defs");
    63 
    61