X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fstyle%2Fproofs.xsl;h=0651f65ec6cdb2224b864010bd8a5025953cbee2;hb=0e25ed1f31b0dd197638e5d212f65d6055656e79;hp=96d1ee7de532142ee3ce9ac18f7e4c6644950351;hpb=0e9cfa8af4ac6569e350dac51b8f8482d124f71a;p=helm.git diff --git a/helm/style/proofs.xsl b/helm/style/proofs.xsl index 96d1ee7de..0651f65ec 100644 --- a/helm/style/proofs.xsl +++ b/helm/style/proofs.xsl @@ -72,6 +72,7 @@ proof + @@ -88,43 +89,99 @@ - + + + - - - - nat_ind - - - - - - - - nat_ind - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - rw_step - + + + + - 7"> @@ -136,7 +193,10 @@ - + + + + @@ -170,7 +230,10 @@ - + + + + @@ -193,8 +256,11 @@ rw_step - - + + + + + @@ -208,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 + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + @@ -298,7 +491,17 @@ - + + + + app + + + + + + + @@ -315,13 +518,34 @@ + + + + + + + . + + + + + - + previous - + + + + + + + . + + + @@ -331,8 +555,6 @@ - - @@ -342,7 +564,15 @@ - + + + + + + . + + + @@ -350,6 +580,23 @@ + + + + + + + + + + + + + + + + +