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/HOL/IMP/Denotation.ML
changeset 4477 b3e5857d8d99
parent 4089 96fba19bcbe2
child 5069 3ea049f7979d
equal deleted inserted replaced
4476:fbdc87f8ac7e 4477:b3e5857d8d99 
    27 
    27 
    28 goal Denotation.thy "!!c s t. <c,s> -c-> t ==> (s,t) : C(c)";
 
    28 goal Denotation.thy "!!c s t. <c,s> -c-> t ==> (s,t) : C(c)";
 
    29 
    29 
    30 (* start with rule induction *)
 
    30 (* start with rule induction *)
 
    31 by (etac evalc.induct 1);
 
    31 by (etac evalc.induct 1);
 
    32 by (Auto_tac());
 
    32 by Auto_tac;
 
    33 (* while *)
 
    33 (* while *)
 
    34 by (rewtac Gamma_def);
 
    34 by (rewtac Gamma_def);
 
    35 by (stac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski)) 1);
 
    35 by (stac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski)) 1);
 
    36 by (Fast_tac 1);
 
    36 by (Fast_tac 1);
 
    37 by (stac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski)) 1);
 
    37 by (stac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski)) 1);
isabelle