src/HOLCF/IOA/meta_theory/Automata.ML
changeset 4477 b3e5857d8d99
parent 4473 803d1e302af1
child 4536 74f7c556fd90
     1.1 --- a/src/HOLCF/IOA/meta_theory/Automata.ML	Tue Dec 23 11:56:09 1997 +0100
     1.2 +++ b/src/HOLCF/IOA/meta_theory/Automata.ML	Wed Dec 24 10:02:30 1997 +0100
     1.3 @@ -112,7 +112,7 @@
     1.4  
     1.5  goal thy"compatible A B = compatible B A";
     1.6  by (asm_full_simp_tac (simpset() addsimps [compatible_def,Int_commute]) 1);
     1.7 -by (Auto_tac());
     1.8 +by Auto_tac;
     1.9  qed"compat_commute";
    1.10  
    1.11  goalw thy [externals_def,actions_def,compatible_def]
    1.12 @@ -289,7 +289,7 @@
    1.13  by (simp_tac (simpset() addsimps [actions_def,asig_internals_def,
    1.14          asig_outputs_def,asig_inputs_def,externals_def,asig_of_def,restrict_def,
    1.15          restrict_asig_def]) 1);
    1.16 -by (Auto_tac());
    1.17 +by Auto_tac;
    1.18  qed"acts_restrict";
    1.19  
    1.20  goal thy "starts_of(restrict ioa acts) = starts_of(ioa) &     \
    1.21 @@ -414,10 +414,11 @@
    1.22  
    1.23  goalw thy [is_trans_of_def,restrict_def,restrict_asig_def] 
    1.24  "!!A. is_trans_of A ==> is_trans_of (rename A f)";
    1.25 -by (asm_full_simp_tac (simpset() addsimps [actions_def,trans_of_def,
    1.26 -    asig_internals_def,asig_outputs_def,asig_inputs_def,externals_def,
    1.27 -   asig_of_def,rename_def,rename_set_def]) 1);
    1.28 -by (Auto_tac());
    1.29 +by (asm_full_simp_tac
    1.30 +    (simpset() addsimps [actions_def,trans_of_def, asig_internals_def,
    1.31 +			 asig_outputs_def,asig_inputs_def,externals_def,
    1.32 +			 asig_of_def,rename_def,rename_set_def]) 1);
    1.33 +by (Blast_tac 1);
    1.34  qed"is_trans_of_rename";
    1.35  
    1.36  goal thy "!! A. [| is_asig_of A; is_asig_of B; compatible A B|]  \
    1.37 @@ -426,7 +427,7 @@
    1.38         asig_comp_def,compatible_def,asig_internals_def,asig_outputs_def,
    1.39       asig_inputs_def,actions_def,is_asig_def]) 1);
    1.40  by (asm_full_simp_tac (simpset() addsimps [asig_of_def]) 1);
    1.41 -by (Auto_tac());
    1.42 +by Auto_tac;
    1.43  by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1));
    1.44  qed"is_asig_of_par";
    1.45  
    1.46 @@ -434,7 +435,7 @@
    1.47             asig_internals_def,asig_outputs_def,asig_inputs_def,externals_def,o_def] 
    1.48  "!! A. is_asig_of A ==> is_asig_of (restrict A f)";
    1.49  by (Asm_full_simp_tac 1);
    1.50 -by (Auto_tac());
    1.51 +by Auto_tac;
    1.52  by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1));
    1.53  qed"is_asig_of_restrict";
    1.54  
    1.55 @@ -442,7 +443,7 @@
    1.56  by (asm_full_simp_tac (simpset() addsimps [is_asig_of_def,
    1.57       rename_def,rename_set_def,asig_internals_def,asig_outputs_def,
    1.58       asig_inputs_def,actions_def,is_asig_def,asig_of_def]) 1);
    1.59 -by (Auto_tac()); 
    1.60 +by Auto_tac; 
    1.61  by (dres_inst_tac [("s","Some xb")] sym 1);
    1.62  by (rotate_tac ~1 1);
    1.63  by (Asm_full_simp_tac 1);
    1.64 @@ -466,7 +467,7 @@
    1.65  "!! A. [|compatible A B; compatible A C |]==> compatible A (B||C)";
    1.66  by (asm_full_simp_tac (simpset() addsimps [internals_of_par, 
    1.67     outputs_of_par,actions_of_par]) 1);
    1.68 -by (Auto_tac());
    1.69 +by Auto_tac;
    1.70  by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1));
    1.71  qed"compatible_par";
    1.72  
    1.73 @@ -475,7 +476,7 @@
    1.74  "!! A. [|compatible A C; compatible B C |]==> compatible (A||B) C";
    1.75  by (asm_full_simp_tac (simpset() addsimps [internals_of_par, 
    1.76     outputs_of_par,actions_of_par]) 1);
    1.77 -by (Auto_tac());
    1.78 +by Auto_tac;
    1.79  by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1));
    1.80  qed"compatible_par2";
    1.81