src/FOL/.fol.thy.ML
author paulson
Thu, 21 Mar 1996 13:02:26 +0100
changeset 1601 0ef6ea27ab15
parent 0 a5a9c433f639
permissions -rw-r--r--
Changes required by removal of the theory argument of Theorem
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
structure FOL =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
struct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
local
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
 val parse_ast_translation = []
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
 val parse_preproc = None
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
 val parse_postproc = None
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
 val parse_translation = []
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
 val print_translation = []
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
 val print_preproc = None
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
 val print_postproc = None
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
 val print_ast_translation = []
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
in
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
(**** begin of user section ****)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
(**** end of user section ****)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
val thy = extend_theory (IFOL.thy)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
 "FOL"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
 ([],
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
  [],
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
  [],
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
  [],
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
  [],
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
  None)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
 [("classical", "(~P ==> P) ==> P")]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
val ax = get_axiom thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
val classical = ax "classical"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
end