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/Resid/Conversion.ML
changeset 4091 771b1f6422a8
parent 3840 e0baea4d485a
child 5068 fb28eaa07e01
equal deleted inserted replaced
4090:9f1eaab75e8c 4091:771b1f6422a8 
    22 
    22 
    23 goal Conversion.thy  
    23 goal Conversion.thy  
    24     "!!u. m<--->n ==> EX p.(m --->p) & (n ---> p)";
 
    24     "!!u. m<--->n ==> EX p.(m --->p) & (n ---> p)";
 
    25 by (etac Sconv.induct 1);
 
    25 by (etac Sconv.induct 1);
 
    26 by (etac Sconv1.induct 1);
 
    26 by (etac Sconv1.induct 1);
 
    27 by (blast_tac (!claset addIs [red1D1,redD2]) 1);
 
    27 by (blast_tac (claset() addIs [red1D1,redD2]) 1);
 
    28 by (blast_tac (!claset addIs [red1D1,redD2]) 1);
 
    28 by (blast_tac (claset() addIs [red1D1,redD2]) 1);
 
    29 by (blast_tac (!claset addIs [red1D1,redD2]) 1);
 
    29 by (blast_tac (claset() addIs [red1D1,redD2]) 1);
 
    30 by (cut_facts_tac [confluence_beta_reduction]  1);
 
    30 by (cut_facts_tac [confluence_beta_reduction]  1);
 
    31 by (rewtac confluence_def);
 
    31 by (rewtac confluence_def);
 
    32 by (blast_tac (!claset addIs [Sred.trans]) 1);
 
    32 by (blast_tac (claset() addIs [Sred.trans]) 1);
 
    33 qed "Church_Rosser";
 
    33 qed "Church_Rosser";
 
    34 
    34
isabelle