src/FOLP/ROOT
author wenzelm
Tue Sep 25 22:36:06 2012 +0200 (2012-09-25 ago)
changeset 49566 66cbf8bb4693
parent 48738 f8c1a5b9488f
child 51397 03b586ee5930
permissions -rw-r--r--
basic integration of graphview into document model;
added Graph_Dockable;
updated Isabelle/jEdit authors and dependencies etc.;
wenzelm@48738
     1
session FOLP = Pure +
wenzelm@48475
     2
  description {*
wenzelm@48475
     3
    Author:     Martin Coen, Cambridge University Computer Laboratory
wenzelm@48475
     4
    Copyright   1993  University of Cambridge
wenzelm@48475
     5
wenzelm@48475
     6
    Modifed version of FOL that contains proof terms.
wenzelm@48475
     7
wenzelm@48475
     8
    Presence of unknown proof term means that matching does not behave as expected.
wenzelm@48475
     9
  *}
wenzelm@48483
    10
  options [document = false]
wenzelm@48475
    11
  theories FOLP
wenzelm@48475
    12
wenzelm@48738
    13
session "FOLP-ex" in ex = FOLP +
wenzelm@48475
    14
  description {*
wenzelm@48475
    15
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
wenzelm@48475
    16
    Copyright   1992  University of Cambridge
wenzelm@48475
    17
wenzelm@48475
    18
    Examples for First-Order Logic.
wenzelm@48475
    19
  *}
wenzelm@48483
    20
  options [document = false]
wenzelm@48475
    21
  theories
wenzelm@48475
    22
    Intro
wenzelm@48475
    23
    Nat
wenzelm@48475
    24
    Foundation
wenzelm@48475
    25
    If
wenzelm@48475
    26
    Intuitionistic
wenzelm@48475
    27
    Classical
wenzelm@48475
    28
    Propositional_Int
wenzelm@48475
    29
    Quantifiers_Int
wenzelm@48475
    30
    Propositional_Cla
wenzelm@48475
    31
    Quantifiers_Cla
wenzelm@48475
    32