isabelle: src/HOL/Modelcheck/MuckeExample1.ML@5e7b6731b004 (annotated)

6466 2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven; mueller parents: diff changeset	1	(* Title: HOL/Modelcheck/MuckeExample1.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	val reach_rws = [INIT_def,N_def,reach_def];
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven; mueller parents: diff changeset	8
7295 fe09a0c5cebe quite a lot of tuning an cleanup; wenzelm parents: 6466 diff changeset	9	Goal "reach (True,True,True)";
6466 2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven; mueller parents: diff changeset	10	by (simp_tac (Mucke_ss addsimps reach_rws) 1);
7295 fe09a0c5cebe quite a lot of tuning an cleanup; wenzelm parents: 6466 diff changeset	11	by (mc_mucke_tac [] 1);
6466 2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven; mueller parents: diff changeset	12	qed "reach_ex_thm1";
2eba94dc5951 added modelchecker mucke besides modelchecker eindhoven; mueller parents: diff changeset	13
7295 fe09a0c5cebe quite a lot of tuning an cleanup; wenzelm parents: 6466 diff changeset	14	(alternative)
fe09a0c5cebe quite a lot of tuning an cleanup; wenzelm parents: 6466 diff changeset	15	Goal "reach (True,True,True)";
fe09a0c5cebe quite a lot of tuning an cleanup; wenzelm parents: 6466 diff changeset	16	by (mc_mucke_tac reach_rws 1);
fe09a0c5cebe quite a lot of tuning an cleanup; wenzelm parents: 6466 diff changeset	17	qed "reach_ex_thm1'";

author	nipkow
	Mon, 06 Jun 2005 19:09:49 +0200
changeset 16305	5e7b6731b004
parent 7295	fe09a0c5cebe
permissions	-rw-r--r--