Removed some type constraints
authornipkow
Tue, 14 Mar 1995 09:43:12 +0100
changeset 231 31040e4345e8
parent 230 e4cccc2dec54
child 232 e22d5a7f5f9f
Removed some type constraints
IOA/ROOT.ML
IOA/meta_theory/IOA.ML
--- a/IOA/ROOT.ML	Tue Mar 14 09:42:49 1995 +0100
+++ b/IOA/ROOT.ML	Tue Mar 14 09:43:12 1995 +0100
@@ -19,4 +19,4 @@
 goals_limit := 1;
 
 loadpath := "IOA/meta_theory" :: "IOA/example" :: !loadpath;
-use_thy "Correctness";
+use_thy "Correctness"  handle _ => exit 1;
--- a/IOA/meta_theory/IOA.ML	Tue Mar 14 09:42:49 1995 +0100
+++ b/IOA/meta_theory/IOA.ML	Tue Mar 14 09:43:12 1995 +0100
@@ -45,7 +45,7 @@
 qed "mk_behaviour_thm";
 
 goalw IOA.thy [reachable_def] "!!A. s:starts_of(A) ==> reachable(A,s)";
-  by (res_inst_tac [("x","<(%i.None),(%i.s)>::('action,'a)execution")] bexI 1);
+  by (res_inst_tac [("x","<%i.None,%i.s>")] bexI 1);
   by (simp_tac SS 1);
   by (asm_simp_tac (SS addsimps exec_rws) 1);
 qed "reachable_0";
@@ -80,8 +80,7 @@
   by (nat_ind_tac "n" 1);
   by (fast_tac (set_cs addIs [p1,reachable_0]) 1);
   by (eres_inst_tac[("x","n1")]allE 1);
-  by (eres_inst_tac[("P","%x.!a::'action.?Q(x,a)"),
-                    ("opt","fst(ex,n1)")] optE 1);
+  by (eres_inst_tac[("P","%x.!a.?Q(x,a)"), ("opt","fst(ex,n1)")] optE 1);
   by (asm_simp_tac HOL_ss 1);
   by (safe_tac HOL_cs);
   by (etac (p2 RS mp) 1);