src/HOL/IOA/IOA.ML
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";