src/HOL/ex/Interpretation_with_Defs.thy
author huffman
Fri Aug 19 14:17:28 2011 -0700 (2011-08-19)
changeset 44311 42c5cbf68052
parent 41582 c34415351b6d
child 46950 d0181abdbdac
permissions -rw-r--r--
Transcendental.thy: add tendsto_intros lemmas;
new isCont theorems;
simplify some proofs.
haftmann@41582
     1
(*  Title:      HOL/ex/Interpretation_with_Defs.thy
haftmann@41582
     2
    Author:     Florian Haftmann, TU Muenchen
haftmann@41582
     3
*)
haftmann@41582
     4
haftmann@41582
     5
header {* Interpretation accompanied with mixin definitions.  EXPERIMENTAL. *}
haftmann@41582
     6
haftmann@41582
     7
theory Interpretation_with_Defs
haftmann@41582
     8
imports Pure
haftmann@41582
     9
uses "~~/src/Tools/interpretation_with_defs.ML"
haftmann@41582
    10
begin
haftmann@41582
    11
haftmann@41582
    12
end