isabelle: src/HOL/Modelcheck/MuckeExample2.ML@6e0f23304061 (annotated)

6466 2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven; mueller parents: diff changeset	1	(* Title: HOL/Modelcheck/MuckeExample2.ML
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven; mueller parents: diff changeset	2	ID: $Id$
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven; mueller parents: diff changeset	3	Author: Olaf Mueller, Jan Philipps, Robert Sandner
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven; mueller parents: diff changeset	4	Copyright 1997 TU Muenchen
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven; mueller parents: diff changeset	5	*)
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven; mueller parents: diff changeset	6
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven; mueller parents: diff changeset	7
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven; mueller parents: diff changeset	8	(* prints the mucke output on the screen *)
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven; mueller parents: diff changeset	9	(* trace_mc := true; *)
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven; mueller parents: diff changeset	10	val Reach_rws = [Init_def,R_def,Reach_def,Reach2_def];
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven; mueller parents: diff changeset	11
7295 fe09a0c5cebe quite a lot of tuning an cleanup; wenzelm parents: 6466 diff changeset	12	Goal "Reach2 True";
6466 2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven; mueller parents: diff changeset	13	by (simp_tac (Mucke_ss addsimps Reach_rws) 1);
7295 fe09a0c5cebe quite a lot of tuning an cleanup; wenzelm parents: 6466 diff changeset	14	by (mc_mucke_tac [] 1);
6466 2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven; mueller parents: diff changeset	15	qed "Reach_thm";
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven; mueller parents: diff changeset	16
7295 fe09a0c5cebe quite a lot of tuning an cleanup; wenzelm parents: 6466 diff changeset	17	(alternative:)
6466 2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven; mueller parents: diff changeset	18	goal thy "Reach2 True";
7295 fe09a0c5cebe quite a lot of tuning an cleanup; wenzelm parents: 6466 diff changeset	19	by (mc_mucke_tac Reach_rws 1);
fe09a0c5cebe quite a lot of tuning an cleanup; wenzelm parents: 6466 diff changeset	20	qed "Reach_thm'";

author	wenzelm
	Thu, 16 Mar 2000 00:35:27 +0100
changeset 8490	6e0f23304061
parent 7295	fe09a0c5cebe
permissions	-rw-r--r--