src/FOL/hypsubstdata.ML
author wenzelm
Fri, 02 Oct 2009 22:15:08 +0200
changeset 32861 105f40051387
parent 27572 67cd6ed76446
child 39159 0dec18004e75
permissions -rw-r--r--
eliminated dead code;
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 =
20974
2a29a21825d1 slight type signature changes
haftmann
parents: 12353
diff changeset
     4
struct
7355
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
     5
  structure Simplifier = Simplifier
21218
38013c3a77a2 tuned hypsubst setup;
wenzelm
parents: 20974
diff changeset
     6
  val dest_eq = FOLogic.dest_eq
7355
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
     7
  val dest_Trueprop = FOLogic.dest_Trueprop
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
     8
  val dest_imp = FOLogic.dest_imp
21539
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 21218
diff changeset
     9
  val eq_reflection = thm "eq_reflection"
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 21218
diff changeset
    10
  val rev_eq_reflection = thm "meta_eq_to_obj_eq"
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 21218
diff changeset
    11
  val imp_intr = thm "impI"
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 21218
diff changeset
    12
  val rev_mp = thm "rev_mp"
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 21218
diff changeset
    13
  val subst = thm "subst"
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 21218
diff changeset
    14
  val sym = thm "sym"
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 21218
diff changeset
    15
  val thin_refl = thm "thin_refl"
27572
67cd6ed76446 single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
krauss
parents: 21539
diff changeset
    16
  val prop_subst = @{lemma "PROP P(t) ==> PROP prop (x = t ==> PROP P(x))"
67cd6ed76446 single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
krauss
parents: 21539
diff changeset
    17
                     by (unfold prop_def) (drule eq_reflection, unfold)}
20974
2a29a21825d1 slight type signature changes
haftmann
parents: 12353
diff changeset
    18
end;
7355
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;