src/FOLP/ex/ROOT.ML
author wenzelm
Sat Jul 25 10:31:27 2009 +0200 (2009-07-25)
changeset 32187 cca43ca13f4f
parent 26408 6964c4799f47
child 35762 af3ff2ba4c54
permissions -rw-r--r--
renamed structure Display_Goal to Goal_Display;
wenzelm@17480
     1
(*  Title:      FOLP/ex/ROOT.ML
clasohm@0
     2
    ID:         $Id$
clasohm@1459
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1992  University of Cambridge
clasohm@0
     5
wenzelm@17480
     6
Examples for First-Order Logic. 
clasohm@0
     7
*)
clasohm@0
     8
wenzelm@25991
     9
use_thys [
wenzelm@25991
    10
  "Intro",
wenzelm@25991
    11
  "Nat",
wenzelm@25991
    12
  "Foundation",
wenzelm@26322
    13
  "If",
wenzelm@26322
    14
  "Intuitionistic",
wenzelm@26408
    15
  "Classical",
wenzelm@26408
    16
  "Propositional_Int",
wenzelm@26408
    17
  "Quantifiers_Int",
wenzelm@26408
    18
  "Propositional_Cla",
wenzelm@26408
    19
  "Quantifiers_Cla"
wenzelm@25991
    20
];