src/FOL/IFOL.ML
author wenzelm
Tue, 13 Sep 2005 22:19:23 +0200
changeset 17339 ab97ccef124a
parent 7355 4c43090659ca
child 18914 5a476b10d69c
permissions -rw-r--r--
tuned Isar interfaces; tuned IsarThy.theorem_i;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
7355
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents: 6966
diff changeset
     2
structure IFOL =
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents: 6966
diff changeset
     3
struct
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents: 6966
diff changeset
     4
  val thy = the_context ();
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents: 6966
diff changeset
     5
  val refl = refl;
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents: 6966
diff changeset
     6
  val subst = subst;
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents: 6966
diff changeset
     7
  val conjI = conjI;
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents: 6966
diff changeset
     8
  val conjunct1 = conjunct1;
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents: 6966
diff changeset
     9
  val conjunct2 = conjunct2;
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents: 6966
diff changeset
    10
  val disjI1 = disjI1;
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents: 6966
diff changeset
    11
  val disjI2 = disjI2;
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents: 6966
diff changeset
    12
  val disjE = disjE;
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents: 6966
diff changeset
    13
  val impI = impI;
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents: 6966
diff changeset
    14
  val mp = mp;
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents: 6966
diff changeset
    15
  val FalseE = FalseE;
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents: 6966
diff changeset
    16
  val True_def = True_def;
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents: 6966
diff changeset
    17
  val not_def = not_def;
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents: 6966
diff changeset
    18
  val iff_def = iff_def;
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents: 6966
diff changeset
    19
  val ex1_def = ex1_def;
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents: 6966
diff changeset
    20
  val allI = allI;
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents: 6966
diff changeset
    21
  val spec = spec;
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents: 6966
diff changeset
    22
  val exI = exI;
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents: 6966
diff changeset
    23
  val exE = exE;
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents: 6966
diff changeset
    24
  val eq_reflection = eq_reflection;
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents: 6966
diff changeset
    25
  val iff_reflection = iff_reflection;
3722
24af9e73451e qed_spec_mp, normalize_thm, etc. copied in from HOL.ML
paulson
parents: 2843
diff changeset
    26
end;
5888
d8e51792ca85 attrib_setup: rulify;
wenzelm
parents: 5309
diff changeset
    27
7355
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents: 6966
diff changeset
    28
open IFOL;