src/HOL/Modelcheck/Example.ML
changeset 3219 9854e3ea09e7
parent 3210 e80db1660614
child 3225 cee363fc07d7
equal deleted inserted replaced
3218:44f01b718eab 3219:9854e3ea09e7
    14 setmp print_mode ["Eindhoven"] pr ();
    14 setmp print_mode ["Eindhoven"] pr ();
    15 
    15 
    16 (*actually invoke the model checker*)
    16 (*actually invoke the model checker*)
    17 by (mc_tac 1);
    17 by (mc_tac 1);
    18 
    18 
    19 qed "reach_ex_thm1";
    19 (*qed "reach_ex_thm1";*)
    20 
    20 
    21 
    21 
    22 
    22 
    23