X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fproofs.xsl;h=0651f65ec6cdb2224b864010bd8a5025953cbee2;hb=e056db635d42bf61eeccbba580c6a0e3a78c3f01;hp=c40a42ce865ac34e19b3b9af7daf04975fb72835;hpb=2ad14dd8ca7dde8d3a5a33ebc466d3ea77b4b6c6;p=helm.git diff --git a/helm/style/proofs.xsl b/helm/style/proofs.xsl index c40a42ce8..0651f65ec 100644 --- a/helm/style/proofs.xsl +++ b/helm/style/proofs.xsl @@ -72,6 +72,7 @@ proof + @@ -88,44 +89,99 @@ - + + + - - - - nat_ind - - - - - - - - nat_ind - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - rw_step - + + + + - 7"> @@ -137,7 +193,10 @@ - + + + + @@ -171,7 +230,10 @@ - + + + + @@ -194,8 +256,11 @@ rw_step - - + + + + + @@ -209,9 +274,19 @@ + + + + false_ind + cic:/Coq/Init/Logic/False_ind.con + + + - - - - or_ind - - - - - + + + + + full_or_ind + + + + left_case + + + + + + + + + + + + right_case + + + + + + + + + + + + + + + or_ind + + + + + + + - + + + + + + + letin + + let + + + + + + + + + + + + - - - - - - - - + + + + + + + rw_step + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + @@ -299,7 +491,17 @@ - + + + + app + + + + + + + @@ -316,13 +518,34 @@ + + + + + + + . + + + + + - + previous - + + + + + + + . + + + @@ -332,8 +555,6 @@ - - @@ -343,7 +564,15 @@ - + + + + + + . + + + @@ -351,6 +580,23 @@ + + + + + + + + + + + + + + + + +