src/HOL/IMP/Natural.ML
changeset 1958 6f20ecbd87cb
parent 1730 1c7f793fc374
child 1973 8c94c9a5be10
equal deleted inserted replaced
1957:58b60b558e48 1958:6f20ecbd87cb
    16                       addEs  [evalc_WHILE_case];
    16                       addEs  [evalc_WHILE_case];
    17 
    17 
    18 (* evaluation of com is deterministic *)
    18 (* evaluation of com is deterministic *)
    19 goal Natural.thy "!!c s t. <c,s> -c-> t ==> (!u. <c,s> -c-> u --> u=t)";
    19 goal Natural.thy "!!c s t. <c,s> -c-> t ==> (!u. <c,s> -c-> u --> u=t)";
    20 by (etac evalc.induct 1);
    20 by (etac evalc.induct 1);
    21 by (eres_inst_tac [("V", "<?c,s2> -c-> s1")] thin_rl 7);
    21 by (thin_tac "<?c,s2> -c-> s1" 7);
    22 by (ALLGOALS (deepen_tac evalc_cs 4));
    22 by (ALLGOALS (deepen_tac evalc_cs 4));
    23 qed_spec_mp "com_det";
    23 qed_spec_mp "com_det";