X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2FDEVEL%2Fmlminidom%2Ftest.xml;fp=helm%2FDEVEL%2Fmlminidom%2Ftest.xml;h=0000000000000000000000000000000000000000;hp=83d2eef68bbdf76d2246b7993d56678810452f8d;hb=869549224eef6278a48c16ae27dd786376082b38;hpb=89262281b6e83bd2321150f81f1a0583645eb0c8 diff --git a/helm/DEVEL/mlminidom/test.xml b/helm/DEVEL/mlminidom/test.xml deleted file mode 100644 index 83d2eef68..000000000 --- a/helm/DEVEL/mlminidom/test.xml +++ /dev/null @@ -1,505 +0,0 @@ - - - - - - - - DEFINITION and_ind() OF TYPE - - - - - - - - __ - - - - - - - - ( - - - - - Π - A - : - - Prop - - - - - - - . - - - - - Π - B - : - - Prop - - - - - - - . - - - - - Π - P - : - - Prop - - - - - - - . - - - - - Π - f - : - - ( - A - → - - ( - B - → - P - ) - - ) - - - - - - - . - - Π - a - : - - ( - and - - _ - - A - - _ - - B - ) - - . - P - - - - - - - - - - - - - - - - - - - - - - - - - - - - :> - - Prop - - - - - - - - ) - - - - - - - - cast - - prod - - A - - - Prop - - - - - prod - - B - - - Prop - - - - - prod - - P - - - Prop - - - - - prod - - f - - - arrow - A - - arrow - B - P - - - - - - prod - - a - - - app - and - A - B - - - - P - - - - - - - Prop - - - - - - - - - - - AS - - - - - - - - __ - - - - - - - λ - A - : - - Prop - - - - - - - . - - - - - λ - B - : - - Prop - - - - - - - . - - - - - λ - P - : - - Prop - - - - - - - . - - - - - λ - f - : - - ( - A - → - - ( - B - → - P - ) - - ) - - - - - - - . - - - - - λ - a - : - - ( - and - - _ - - A - - _ - - B - ) - - - - - - - . - - < - P - > - CASES - - _ - - a - - _ - - OF - - ( - conj - - _ - - $1 - - _ - - $2 - ) - - ⇒ - - ( - f - - _ - - $1 - - _ - - $2 - ) - - - _ - - END - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - A - - - Prop - - - - - - B - - - Prop - - - - - - P - - - Prop - - - - - - f - - - arrow - A - - arrow - B - P - - - - - - - a - - - app - and - A - B - - - - - mutcase - P - a - - app - conj - $1 - $2 - - - app - f - $1 - $2 - - - - - - - - - - - - - -