--- a/src/HOL/IOA/meta_theory/IOA.ML Mon Sep 23 18:26:51 1996 +0200
+++ b/src/HOL/IOA/meta_theory/IOA.ML Tue Sep 24 08:59:24 1996 +0200
@@ -6,6 +6,8 @@
The I/O automata of Lynch and Tuttle.
*)
+Addsimps [Let_def];
+
open IOA Asig;
val ioa_projections = [asig_of_def, starts_of_def, trans_of_def];
@@ -81,7 +83,7 @@
by (nat_ind_tac "n" 1);
by (fast_tac (!claset addIs [p1,reachable_0]) 1);
by (eres_inst_tac[("x","n1")]allE 1);
- by (eres_inst_tac[("P","%x.!a.?Q x a"), ("opt","fst ex n1")] optE 1);
+ by (eres_inst_tac[("P","%x.!a.?Q x a"), ("opt","fst ex n1")] optionE 1);
by (Asm_simp_tac 1);
by (safe_tac (!claset));
by (etac (p2 RS mp) 1);