lib/html/index2.html
author berghofe
Thu, 07 Aug 1997 23:32:24 +0200
changeset 3634 fc9970e62cfa
child 3740 26992736d471
permissions -rw-r--r--
Index file which is copied to $ISABELLE_BROWSER_INFO when theory browsing data is generated.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3634
fc9970e62cfa Index file which is copied to $ISABELLE_BROWSER_INFO
berghofe
parents:
diff changeset
     1
<HTML><HEAD><TITLE>Isabelle Logics</TITLE></HEAD>
fc9970e62cfa Index file which is copied to $ISABELLE_BROWSER_INFO
berghofe
parents:
diff changeset
     2
<center>
fc9970e62cfa Index file which is copied to $ISABELLE_BROWSER_INFO
berghofe
parents:
diff changeset
     3
 <H2>
fc9970e62cfa Index file which is copied to $ISABELLE_BROWSER_INFO
berghofe
parents:
diff changeset
     4
 <img src="../gif/Isabelle.gif"><P>
fc9970e62cfa Index file which is copied to $ISABELLE_BROWSER_INFO
berghofe
parents:
diff changeset
     5
 <i>The Logical Choice!</i>
fc9970e62cfa Index file which is copied to $ISABELLE_BROWSER_INFO
berghofe
parents:
diff changeset
     6
 </H2>
fc9970e62cfa Index file which is copied to $ISABELLE_BROWSER_INFO
berghofe
parents:
diff changeset
     7
</center>
fc9970e62cfa Index file which is copied to $ISABELLE_BROWSER_INFO
berghofe
parents:
diff changeset
     8
<P>
fc9970e62cfa Index file which is copied to $ISABELLE_BROWSER_INFO
berghofe
parents:
diff changeset
     9
<A HREF="../html/index.html">View version for non-Java-capable browsers</A>
fc9970e62cfa Index file which is copied to $ISABELLE_BROWSER_INFO
berghofe
parents:
diff changeset
    10
<P>
fc9970e62cfa Index file which is copied to $ISABELLE_BROWSER_INFO
berghofe
parents:
diff changeset
    11
Click on the logic's name to view the graph of its theories.
fc9970e62cfa Index file which is copied to $ISABELLE_BROWSER_INFO
berghofe
parents:
diff changeset
    12
<HR>
fc9970e62cfa Index file which is copied to $ISABELLE_BROWSER_INFO
berghofe
parents:
diff changeset
    13
First-Order Logic
fc9970e62cfa Index file which is copied to $ISABELLE_BROWSER_INFO
berghofe
parents:
diff changeset
    14
  <UL>
fc9970e62cfa Index file which is copied to $ISABELLE_BROWSER_INFO
berghofe
parents:
diff changeset
    15
  <LI><A HREF = "data/FOL/all_theories.html">FOL</A>
fc9970e62cfa Index file which is copied to $ISABELLE_BROWSER_INFO
berghofe
parents:
diff changeset
    16
  <LI><A HREF = "data/ZF/all_theories.html">ZF (Set Theory)</A>
fc9970e62cfa Index file which is copied to $ISABELLE_BROWSER_INFO
berghofe
parents:
diff changeset
    17
  <LI><A HREF = "data/CCL/all_theories.html">CCL (Classical Computational Logic)</A>
fc9970e62cfa Index file which is copied to $ISABELLE_BROWSER_INFO
berghofe
parents:
diff changeset
    18
  <LI><A HREF = "data/LCF/all_theories.html">LCF (Logic of Computable Functions)</A>
fc9970e62cfa Index file which is copied to $ISABELLE_BROWSER_INFO
berghofe
parents:
diff changeset
    19
  <LI><A HREF = "data/FOLP/all_theories.html">FOLP (FOL with Proof Terms)</A>
fc9970e62cfa Index file which is copied to $ISABELLE_BROWSER_INFO
berghofe
parents:
diff changeset
    20
  </UL>
fc9970e62cfa Index file which is copied to $ISABELLE_BROWSER_INFO
berghofe
parents:
diff changeset
    21
<HR>
fc9970e62cfa Index file which is copied to $ISABELLE_BROWSER_INFO
berghofe
parents:
diff changeset
    22
Higher-Order Logic
fc9970e62cfa Index file which is copied to $ISABELLE_BROWSER_INFO
berghofe
parents:
diff changeset
    23
  <UL>
fc9970e62cfa Index file which is copied to $ISABELLE_BROWSER_INFO
berghofe
parents:
diff changeset
    24
  <LI><A HREF = "data/HOL/all_theories.html">HOL</A>
fc9970e62cfa Index file which is copied to $ISABELLE_BROWSER_INFO
berghofe
parents:
diff changeset
    25
  <LI><A HREF = "data/HOLCF/all_theories.html">HOLCF 
fc9970e62cfa Index file which is copied to $ISABELLE_BROWSER_INFO
berghofe
parents:
diff changeset
    26
		   (Higher-Order Logic of Computable Functions)</A>
fc9970e62cfa Index file which is copied to $ISABELLE_BROWSER_INFO
berghofe
parents:
diff changeset
    27
  </UL>
fc9970e62cfa Index file which is copied to $ISABELLE_BROWSER_INFO
berghofe
parents:
diff changeset
    28
<HR>
fc9970e62cfa Index file which is copied to $ISABELLE_BROWSER_INFO
berghofe
parents:
diff changeset
    29
Miscellaneous
fc9970e62cfa Index file which is copied to $ISABELLE_BROWSER_INFO
berghofe
parents:
diff changeset
    30
  <UL>
fc9970e62cfa Index file which is copied to $ISABELLE_BROWSER_INFO
berghofe
parents:
diff changeset
    31
  <LI><A HREF = "data/Sequents/all_theories.html">Sequents 
fc9970e62cfa Index file which is copied to $ISABELLE_BROWSER_INFO
berghofe
parents:
diff changeset
    32
	  (first-order, modal and linear logics)</A>
fc9970e62cfa Index file which is copied to $ISABELLE_BROWSER_INFO
berghofe
parents:
diff changeset
    33
  <LI><A HREF = "data/CTT/all_theories.html">CTT (Constructive Type Theory)</A>
fc9970e62cfa Index file which is copied to $ISABELLE_BROWSER_INFO
berghofe
parents:
diff changeset
    34
  <LI><A HREF = "data/Cube/all_theories.html">Cube (The Lambda Cube)</A>
fc9970e62cfa Index file which is copied to $ISABELLE_BROWSER_INFO
berghofe
parents:
diff changeset
    35
  </UL>
fc9970e62cfa Index file which is copied to $ISABELLE_BROWSER_INFO
berghofe
parents:
diff changeset
    36
<HR>
fc9970e62cfa Index file which is copied to $ISABELLE_BROWSER_INFO
berghofe
parents:
diff changeset
    37
</BODY></HTML>