src/FOL/.fol.thy.ML
author wenzelm
Sun, 15 Oct 2000 19:50:35 +0200
changeset 10220 2a726de6e124
parent 0 a5a9c433f639
permissions -rw-r--r--
proper symbol markup with \isamath, \isatext; support sub/super scripts:
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