src/HOL/IOA/Solve.ML
changeset 5132 24f992a25adc
parent 5069 3ea049f7979d
child 5143 b94cd208f073
     1.1 --- a/src/HOL/IOA/Solve.ML	Fri Jul 10 15:24:22 1998 +0200
     1.2 +++ b/src/HOL/IOA/Solve.ML	Sun Jul 12 11:49:17 1998 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4  \          is_weak_pmap f C A |] ==> traces(C) <= traces(A)";
     1.5  
     1.6    by (simp_tac(simpset() addsimps [has_trace_def])1);
     1.7 -  by (Safe_tac);
     1.8 +  by Safe_tac;
     1.9    by (rename_tac "ex1 ex2" 1);
    1.10  
    1.11    (* choose same trace, therefore same NF *)