src/HOL/IOA/Solve.ML
changeset 5069 3ea049f7979d
parent 4838 196100237656
child 5132 24f992a25adc
     1.1 --- a/src/HOL/IOA/Solve.ML	Mon Jun 22 17:13:09 1998 +0200
     1.2 +++ b/src/HOL/IOA/Solve.ML	Mon Jun 22 17:26:46 1998 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4  
     1.5  Addsimps [mk_trace_thm,trans_in_actions];
     1.6  
     1.7 -goalw Solve.thy [is_weak_pmap_def,traces_def]
     1.8 +Goalw [is_weak_pmap_def,traces_def]
     1.9    "!!f. [| IOA(C); IOA(A); externals(asig_of(C)) = externals(asig_of(A)); \
    1.10  \          is_weak_pmap f C A |] ==> traces(C) <= traces(A)";
    1.11  
    1.12 @@ -65,7 +65,7 @@
    1.13   by (Fast_tac 1);
    1.14  val externals_of_par_extra = result(); 
    1.15  
    1.16 -goal Solve.thy "!!s.[| reachable (C1||C2) s |] ==> reachable C1 (fst s)";
    1.17 +Goal "!!s.[| reachable (C1||C2) s |] ==> reachable C1 (fst s)";
    1.18  by (asm_full_simp_tac (simpset() addsimps [reachable_def]) 1); 
    1.19  by (etac bexE 1);
    1.20  by (res_inst_tac [("x",
    1.21 @@ -85,7 +85,7 @@
    1.22  
    1.23  (* Exact copy of proof of comp1_reachable for the second 
    1.24     component of a parallel composition.     *)
    1.25 -goal Solve.thy "!!s.[| reachable (C1||C2) s|] ==> reachable C2 (snd s)";
    1.26 +Goal "!!s.[| reachable (C1||C2) s|] ==> reachable C2 (snd s)";
    1.27  by (asm_full_simp_tac (simpset() addsimps [reachable_def]) 1); 
    1.28  by (etac bexE 1);
    1.29  by (res_inst_tac [("x",
    1.30 @@ -105,7 +105,7 @@
    1.31  Delsplits [split_if];
    1.32  
    1.33  (* Composition of possibility-mappings *)
    1.34 -goalw Solve.thy [is_weak_pmap_def] "!!f g.[| is_weak_pmap f C1 A1 & \
    1.35 +Goalw [is_weak_pmap_def] "!!f g.[| is_weak_pmap f C1 A1 & \
    1.36  \               externals(asig_of(A1))=externals(asig_of(C1)) &\
    1.37  \               is_weak_pmap g C2 A2 &  \
    1.38  \               externals(asig_of(A2))=externals(asig_of(C2)) & \
    1.39 @@ -149,7 +149,7 @@
    1.40  qed"fxg_is_weak_pmap_of_product_IOA";
    1.41  
    1.42  
    1.43 -goal Solve.thy "!!s.[| reachable (rename C g) s |] ==> reachable C s";
    1.44 +Goal "!!s.[| reachable (rename C g) s |] ==> reachable C s";
    1.45  by (asm_full_simp_tac (simpset() addsimps [reachable_def]) 1); 
    1.46  by (etac bexE 1);
    1.47  by (res_inst_tac [("x",
    1.48 @@ -166,7 +166,7 @@
    1.49  qed"reachable_rename_ioa";
    1.50  
    1.51  
    1.52 -goal Solve.thy "!!f.[| is_weak_pmap f C A |]\
    1.53 +Goal "!!f.[| is_weak_pmap f C A |]\
    1.54  \                      ==> (is_weak_pmap f (rename C g) (rename A g))";
    1.55  by (asm_full_simp_tac (simpset() addsimps [is_weak_pmap_def]) 1);
    1.56  by (rtac conjI 1);