src/FOL/hypsubstdata.ML
author wenzelm
Tue, 04 Dec 2001 02:00:45 +0100
changeset 12353 e4be26df707a
parent 12345 5d1436d1c268
child 20974 2a29a21825d1
permissions -rw-r--r--
no need for hyp_subst_tac' (!?);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7355
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
     1
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
     2
(** Applying HypsubstFun to generate hyp_subst_tac **)
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
     3
structure Hypsubst_Data =
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
     4
  struct
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
     5
  structure Simplifier = Simplifier
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
     6
    (*These destructors  Match!*)
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
     7
  fun dest_eq (Const("op =",T)  $ t $ u) = (t, u, domain_type T)
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
     8
  val dest_Trueprop = FOLogic.dest_Trueprop
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
     9
  val dest_imp = FOLogic.dest_imp
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    10
  val eq_reflection = eq_reflection
9528
95852b4be214 rev_eq_reflection = meta_eq_to_obj_eq;
wenzelm
parents: 7355
diff changeset
    11
  val rev_eq_reflection = meta_eq_to_obj_eq
7355
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    12
  val imp_intr = impI
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    13
  val rev_mp = rev_mp
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    14
  val subst = subst
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    15
  val sym = sym
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    16
  val thin_refl = prove_goal (the_context ())
12353
e4be26df707a no need for hyp_subst_tac' (!?);
wenzelm
parents: 12345
diff changeset
    17
                  "!!X. [|x=x; PROP W|] ==> PROP W" (K [atac 1]);
7355
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    18
  end;
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    19
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    20
structure Hypsubst = HypsubstFun(Hypsubst_Data);
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    21
open Hypsubst;