Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/ZF/ex/BinEx.ML
changeset 9548 15bee2731e43
parent 9000 c20d58286a51
child 9570 e16e168984e1
equal deleted inserted replaced
9547:8dad21f06b24 9548:15bee2731e43 
    24 
    24 
    25 Goal "#93746  $+  #-46375 = #47371";
 
    25 Goal "#93746  $+  #-46375 = #47371";
 
    26 by (Simp_tac 1);    (*300 msec*)
 
    26 by (Simp_tac 1);    (*300 msec*)
 
    27 result();
 
    27 result();
 
    28 
    28 
    29 Goal "$~ #65745 = #-65745";
 
    29 Goal "$- #65745 = #-65745";
 
    30 by (Simp_tac 1);    (*80 msec*)
 
    30 by (Simp_tac 1);    (*80 msec*)
 
    31 result();
 
    31 result();
 
    32 
    32 
    33 (* negation of ~54321 *)
 
    33 (* negation of ~54321 *)
 
    34 Goal "$~ #-54321 = #54321";
 
    34 Goal "$- #-54321 = #54321";
 
    35 by (Simp_tac 1);    (*90 msec*)
 
    35 by (Simp_tac 1);    (*90 msec*)
 
    36 result();
 
    36 result();
 
    37 
    37 
    38 Goal "#13  $*  #19 = #247";
 
    38 Goal "#13  $*  #19 = #247";
 
    39 by (Simp_tac 1);    (*110 msec*)
 
    39 by (Simp_tac 1);    (*110 msec*)
isabelle