src/HOL/UNITY/LessThan.ML
changeset 7521 a18adacbdbd2
parent 6825 30e09714eef5
child 7878 43b03d412b82
equal deleted inserted replaced
7520:65f0cec65fc6 7521:a18adacbdbd2
    41 Goalw [lessThan_def, atLeast_def, le_def]
    41 Goalw [lessThan_def, atLeast_def, le_def]
    42     "-lessThan k = atLeast k";
    42     "-lessThan k = atLeast k";
    43 by (Blast_tac 1);
    43 by (Blast_tac 1);
    44 qed "Compl_lessThan";
    44 qed "Compl_lessThan";
    45 
    45 
       
    46 Goal "{k} - lessThan k = {k}";
       
    47 by (Blast_tac 1);
       
    48 qed "single_Diff_lessThan";
       
    49 Addsimps [single_Diff_lessThan];
    46 
    50 
    47 (*** greaterThan ***)
    51 (*** greaterThan ***)
    48 
    52 
    49 Goalw [greaterThan_def] "(i: greaterThan k) = (k<i)";
    53 Goalw [greaterThan_def] "(i: greaterThan k) = (k<i)";
    50 by (Blast_tac 1);
    54 by (Blast_tac 1);