--- a/src/HOL/IOA/Solve.ML Mon Jun 22 17:13:09 1998 +0200
+++ b/src/HOL/IOA/Solve.ML Mon Jun 22 17:26:46 1998 +0200
@@ -10,7 +10,7 @@
Addsimps [mk_trace_thm,trans_in_actions];
-goalw Solve.thy [is_weak_pmap_def,traces_def]
+Goalw [is_weak_pmap_def,traces_def]
"!!f. [| IOA(C); IOA(A); externals(asig_of(C)) = externals(asig_of(A)); \
\ is_weak_pmap f C A |] ==> traces(C) <= traces(A)";
@@ -65,7 +65,7 @@
by (Fast_tac 1);
val externals_of_par_extra = result();
-goal Solve.thy "!!s.[| reachable (C1||C2) s |] ==> reachable C1 (fst s)";
+Goal "!!s.[| reachable (C1||C2) s |] ==> reachable C1 (fst s)";
by (asm_full_simp_tac (simpset() addsimps [reachable_def]) 1);
by (etac bexE 1);
by (res_inst_tac [("x",
@@ -85,7 +85,7 @@
(* Exact copy of proof of comp1_reachable for the second
component of a parallel composition. *)
-goal Solve.thy "!!s.[| reachable (C1||C2) s|] ==> reachable C2 (snd s)";
+Goal "!!s.[| reachable (C1||C2) s|] ==> reachable C2 (snd s)";
by (asm_full_simp_tac (simpset() addsimps [reachable_def]) 1);
by (etac bexE 1);
by (res_inst_tac [("x",
@@ -105,7 +105,7 @@
Delsplits [split_if];
(* Composition of possibility-mappings *)
-goalw Solve.thy [is_weak_pmap_def] "!!f g.[| is_weak_pmap f C1 A1 & \
+Goalw [is_weak_pmap_def] "!!f g.[| is_weak_pmap f C1 A1 & \
\ externals(asig_of(A1))=externals(asig_of(C1)) &\
\ is_weak_pmap g C2 A2 & \
\ externals(asig_of(A2))=externals(asig_of(C2)) & \
@@ -149,7 +149,7 @@
qed"fxg_is_weak_pmap_of_product_IOA";
-goal Solve.thy "!!s.[| reachable (rename C g) s |] ==> reachable C s";
+Goal "!!s.[| reachable (rename C g) s |] ==> reachable C s";
by (asm_full_simp_tac (simpset() addsimps [reachable_def]) 1);
by (etac bexE 1);
by (res_inst_tac [("x",
@@ -166,7 +166,7 @@
qed"reachable_rename_ioa";
-goal Solve.thy "!!f.[| is_weak_pmap f C A |]\
+Goal "!!f.[| is_weak_pmap f C A |]\
\ ==> (is_weak_pmap f (rename C g) (rename A g))";
by (asm_full_simp_tac (simpset() addsimps [is_weak_pmap_def]) 1);
by (rtac conjI 1);