From 76ef6920890304b5c840d9869952f52c0263be73 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 8 Apr 2003 15:16:45 +0000 Subject: [PATCH] nuprl_content_to_html.xsl is not used. Let's definitely remove it. --- .../nuprl_content_to_html.xsl | 2807 ----------------- helm/nuprl_stylesheets/xslt_index.txt | 1 - 2 files changed, 2808 deletions(-) delete mode 100644 helm/nuprl_stylesheets/nuprl_content_to_html.xsl diff --git a/helm/nuprl_stylesheets/nuprl_content_to_html.xsl b/helm/nuprl_stylesheets/nuprl_content_to_html.xsl deleted file mode 100644 index a2dbe9c03..000000000 --- a/helm/nuprl_stylesheets/nuprl_content_to_html.xsl +++ /dev/null @@ -1,2807 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - Ax - - - - - Void - - - - - - - - " - ∀ - ??? - - - - - - l - λ - ??? - - - - - - Õ - Π - ??? - - - - - - ® - → - ??? - - - - - - Þ - ⇒ - ??? - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - <xsl:value-of select="$CICURI"/> - - - - - - if(document.getElementById) - for(var i=0;i<document.to_be_deleted.length;i++) - Hide(document.getElementById(document.to_be_deleted[i])); - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -

- - - - - - - "" - - - : - - - ( - - - - ) - - - - - - - - - - - - - - - - - - : - - ( - - - - ) - - . - - - ) - - - - - - - - : - - - x - - - - - - - - - x - - - - - - - - < - - - , - - - > - - - - - - - - + - - - - - - - - inl ( - - - - ) - - - - - - - inr ( - - - - ) - - - - - - - - = - - - - - - - - - - - - - - - - - - - - :: - - - - - - - - - rectype - - - - = - - - - - - - - - - { - - - - - - : - - - - - - - - - | - - - - - - - - - - - - - - - : - - - - . - - - - - - - - - , - - - : - - - - // - - - - - - - ( - - - - - - - - ) - - - - - ( - - - - - - ) - - - - ( - - :> - - ) - - - Prop - - - Set - - - Type - - - - - < - - > - CASE - - OF - - - - - | - - - - - - - - - - - - - - - FIX - - { - - - : - - := - - - - } - - - ; - - - - - - - - COFIX - - { - - - : - - := - - - - } - - - ; - - - - - - - - - proves - - - - letin1 (inline error) - - - - - Contradiction. - - - - From - - we get - ( - - ) - - and - ( - - ) - - ; - hence - - - - - - - - - - - - - - - - - : - - - . - - - - - - - - - - - - - - - - - - -

- - - - - - - - : - - ( - - - - -
- - - - - - - - - - - - - ( - - - - - - - - - - - - : - - - - ( - - - - ) - - -
- - - - - - - - - - - - - - - - - : - - - -
- - - - . - - - - - - - - - - - - - - - - - - - - - : - - -
- - - - . - - - - - - - - - - - - - - - - - - - - - -
- - - - . - - - - - - - - - - - - - - - - < - - - - - , -
- - - - - - > - - - - - - - - - - - - - - - -
- - - - - + - - - - - - - - - - - - - - - inl ( - - - - -
- - - - - ) - - - - - - - - - - - - - - inr ( - - - - -
- - - - - ) - - - - - - - - - - - - P - - - - - - - - - - U - - - - - - - - - - - - - = - - - - -
- - - - - - - - - - - - - - - - - - - - - - - - " - - - - " - - - - - - - - [] - - - - - - - - -
- - - - - :: - - - - - - - - - - rectype - - - - -
- - - - - = - - - - - - - - - { - - - - - - : - - - - -
- - - - - - - - - -
- - - - - - - | - - - - - - - - - - - - - - - : - - - - -
- - - - - . - - - - - - - - - , - - - : - - - - -
- - - - - // - - - - - - - - - - - atom_eq ( - - - - - int_eq ( - - - - - less ( - - - - - ; - - ; - - ; - - - ) - - - - - - - - - - - spread ( - - - ; - - , - - . - - - ) - - - - - - decide ( - - - ; - - . - - ; - - . - - - ) - - - - - any ( - - - - ) - - - - - - - - - so_ - - - - - - - - - - ( - - - , - - - ) - - -

- . - -

- - - - - - - - so_apply - ( - - - - - - ) - - - - - - - - - - - ( - - - -
- - - - - - - - - - - - - ) - - - - - - - - - - - - ( - - - - -
- - - - - - - - ) - - - - - - - - - - - - - ( - - -
- - - :> - - - - ) - - - - - - - - - - - - - - - Prop - - - Set - - - Type - - - - - < - - - - > -
- - - CASE - - - - OF - - -
- - - - - - - - - | - - - - - - - - - - - - - -
- - - - - - - - - - - - - - - - - - - - - - - FIX - - { - -
- - - - - : - - - -
- - - - := - - - - -
- - - - } - - - - - - - - - - - COFIX - - { -
- - - - - - : - - - -
- - - - := - - - - - -
- - - - } - - - - - - - - let - - := - - - -
- - - - in - - - - - - - - - - - - - - - - - - - - - - -
- - - - we proved - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - We have the following equality chain: - - -
- - - - - - - - - = - - - = - - - - - - -
- - - - - - - - - - - - We have the following chain of disequalities: - - -
- - - - - - - - - - - - - - - - - - - - -
- - - - - - - - - - - - - - -
- - - - - - - - - - - - - -
- - - - - - - - - - - ( - - ) - - - - - - - - - - - - - - Consider - - - - - - - - - - - - - - - - - - -
- - - - Rewrite - - - -
- - - - - with - - - -
- - - - - by - - - - - - - - - -
- - - - Then apply it to - - - - - We prove - - - -
- - - - by induction on - - - - - - - - - - - -
- - - - Case - - - - -
- - - - By induction hypothesis, we have: - -
- - - - ( - - ) - - - - - -
- - - - - - - - - - - - - - - - ( - - - - - : - - - ) - - - - - - - - -
- - - - Contradiction. - - - - - - - - - - - Consider - - - -
- - - - In particular, we have -
- - - - ( - - ) - - - -
- - - - ( - - ) - - - -
- - - - - - - - - - - - - - - - - Consider - - - -
- - - - We proceed by cases to prove - -
- - - - Left: suppose - ( - - ) - -
- - - - - - -
- - - - Right: suppose - ( - - ) - -
- - - - - - - - - - - - - - - - - Consider - - - -
- - - - We prove - - by cases: -
- - - - Left: - - - -
- - - - Right: - - - - - - - - - - - - - - Consider - - - - - -
- - - - Let - - : - - such that -
- - - - ( - - ) - - - -
- - - - - - - - - - - - - [ - - - - - - - - - - - - - - - - - - - - - ] - - - - _{-
-} - - - - - - - - - - - - - - - - - - - ^{-
-} - ( - - ) - - - - - - - - - - - - - - - - - - - - - - ^{-
-} - ( - - ) - - - - - - - - - - - - - - _{-
-
-
-
-
-} - - - - - - - - - _{-
-
-
-
-
-} - - - - - - - - - - - - - - - - _{-
-
-
-
-
- *
-} - - - - - - - - - _{-
-
-
-
-
- *
-} - - - - - - - - - - - - - - - - _{-
-
-
-
-
-} - - - - - - - - - _{-
-
-
-
-
-} - - - - - - - - - - - - - - - - _{-
-
-
-
-
- *
-} - - - - - - - - - _{-
-
-
-
-
- *
-} - - - - - - - - - - | - - - | - - - - - - | - - - | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - [ - - ] - - - - - - - - - - - - - - - - - - - - - - - - - : - - -
- - - - . - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - ( - - - - - - - - - - ) - - - - - - - - -

- - - - - - - - - - - - - - - - - - - - - - -

- - -

- - - - - - - - - - - - - - - - - - - - - - - - - - -

-Rule: -
- - - - - - - - - - ( - - - - - level-exp( - - ) - - - - - - - - - - , - - - - ) - - - -

- - - - - - -

-Sequent () : -
- - - - - ) - - ( - - - - - - - - - - - ) - - - -
- -===================================== -
- - - - -

- - - - - - - -

-Node:
- - - - - -

- - - - - - - -

-DEFINITION ()
-TYPE =
- - - - - -
-BODY =
- - - - - - -

- - - - - - -

-AXIOM ()
-TYPE =
- - - - - - -

- - - - - - -

-UNFINISHED PROOF ()
-THESIS: - -
-CONJECTURES: - -
- - - - - - - - - - - - _ - - - : - - - - - - - - - - - _ - - - := - - - - - - _ :? _ - - - - |- : - - - - -
-PROOF: - - - -

- - - - - - -

- - - - - - INDUCTIVE DEFINITION - - - COINDUCTIVE DEFINITION - - - - - AND - - - () - [ - - - - : - - - - ]
- OF ARITY - - -
- BUILT FROM: - -
- - - - - - - - - | - - - - : - - - - - -

- - - - - - -

-VARIABLE
-TYPE = - - - -
-BODY = - - - -

- - - - - - - - - - -

BEGIN OF SECTION

- -

END OF SECTION

- - - diff --git a/helm/nuprl_stylesheets/xslt_index.txt b/helm/nuprl_stylesheets/xslt_index.txt index 11e49a8ea..d193b316d 100644 --- a/helm/nuprl_stylesheets/xslt_index.txt +++ b/helm/nuprl_stylesheets/xslt_index.txt @@ -2,7 +2,6 @@ nuprl_abstract.xsl nuprl_proof.xsl nuprl_rules.xsl nuprl_term.xsl -nuprl_content_to_html.xsl nuprl_content_to_html2.xsl nuprl_annotatedpres.xsl nuprl_mmlextension.xsl -- 2.39.2