src/HOL/Modelcheck/MuckeExample2.ML
author paulson
Tue Jun 28 15:27:45 2005 +0200 (2005-06-28)
changeset 16587 b34c8aa657a5
parent 7295 fe09a0c5cebe
permissions -rw-r--r--
Constant "If" is now local
     1 (*  Title:      HOL/Modelcheck/MuckeExample2.ML
     2     ID:         $Id$
     3     Author:     Olaf Mueller, Jan Philipps, Robert Sandner
     4     Copyright   1997  TU Muenchen
     5 *)
     6 
     7 
     8 (* prints the mucke output on the screen *)
     9 (* trace_mc := true; *)
    10 val Reach_rws = [Init_def,R_def,Reach_def,Reach2_def];
    11 
    12 Goal "Reach2 True";
    13 by (simp_tac (Mucke_ss addsimps Reach_rws) 1);
    14 by (mc_mucke_tac [] 1);
    15 qed "Reach_thm";
    16 
    17 (*alternative:*)
    18 goal thy "Reach2 True";
    19 by (mc_mucke_tac Reach_rws 1);
    20 qed "Reach_thm'";