| changeset 8114 | 09a7a180cc99 | 
| parent 7499 | 23e090051cb8 | 
| child 8423 | 3c19160b6432 | 
--- a/src/HOL/IOA/IOA.ML Fri Jan 07 11:04:15 2000 +0100 +++ b/src/HOL/IOA/IOA.ML Fri Jan 07 11:06:03 2000 +0100 @@ -15,7 +15,7 @@ val exec_rws = [executions_def,is_execution_fragment_def]; Goal -"asig_of((x,y,z)) = x & starts_of((x,y,z)) = y & trans_of((x,y,z)) = z"; +"asig_of(x,y,z) = x & starts_of(x,y,z) = y & trans_of(x,y,z) = z"; by (simp_tac (simpset() addsimps ioa_projections) 1); qed "ioa_triple_proj";