isabelle: src/HOLCF/IOA/Modelcheck/MuIOAOracle.thy@0b2ff9541727 (annotated)

7299 743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	1
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 7299 diff changeset	2	(* $Id$ *)
6471 08d12ef5fc19 added translation from IOA to mucalculus and corresponding modelchecker examples; mueller parents: diff changeset	3
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 7299 diff changeset	4	theory MuIOAOracle
0b2ff9541727 converted to Isar theory format; wenzelm parents: 7299 diff changeset	5	imports MuIOA
0b2ff9541727 converted to Isar theory format; wenzelm parents: 7299 diff changeset	6	begin
0b2ff9541727 converted to Isar theory format; wenzelm parents: 7299 diff changeset	7
0b2ff9541727 converted to Isar theory format; wenzelm parents: 7299 diff changeset	8	oracle sim_oracle ("term * thm list") =
0b2ff9541727 converted to Isar theory format; wenzelm parents: 7299 diff changeset	9	mk_sim_oracle
6471 08d12ef5fc19 added translation from IOA to mucalculus and corresponding modelchecker examples; mueller parents: diff changeset	10
08d12ef5fc19 added translation from IOA to mucalculus and corresponding modelchecker examples; mueller parents: diff changeset	11	end