src/HOL/Typedef.thy
changeset 29797 08ef36ed2f8a
parent 29608 564ea783ace8
child 31723 f5cafe803b55
     1.1 --- a/src/HOL/Typedef.thy	Tue Feb 03 19:48:06 2009 +0100
     1.2 +++ b/src/HOL/Typedef.thy	Tue Feb 03 21:26:21 2009 +0100
     1.3 @@ -119,52 +119,4 @@
     1.4  use "Tools/typecopy_package.ML" setup TypecopyPackage.setup
     1.5  use "Tools/typedef_codegen.ML" setup TypedefCodegen.setup
     1.6  
     1.7 -
     1.8 -text {* This class is just a workaround for classes without parameters;
     1.9 -  it shall disappear as soon as possible. *}
    1.10 -
    1.11 -class itself = 
    1.12 -  fixes itself :: "'a itself"
    1.13 -
    1.14 -setup {*
    1.15 -let fun add_itself tyco thy =
    1.16 -  let
    1.17 -    val vs = Name.names Name.context "'a"
    1.18 -      (replicate (Sign.arity_number thy tyco) @{sort type});
    1.19 -    val ty = Type (tyco, map TFree vs);
    1.20 -    val lhs = Const (@{const_name itself}, Term.itselfT ty);
    1.21 -    val rhs = Logic.mk_type ty;
    1.22 -    val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
    1.23 -  in
    1.24 -    thy
    1.25 -    |> TheoryTarget.instantiation ([tyco], vs, @{sort itself})
    1.26 -    |> `(fn lthy => Syntax.check_term lthy eq)
    1.27 -    |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq)))
    1.28 -    |> snd
    1.29 -    |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
    1.30 -    |> LocalTheory.exit_global
    1.31 -  end
    1.32 -in TypedefPackage.interpretation add_itself end
    1.33 -*}
    1.34 -
    1.35 -instantiation bool :: itself
    1.36 -begin
    1.37 -
    1.38 -definition "itself = TYPE(bool)"
    1.39 -
    1.40 -instance ..
    1.41 -
    1.42  end
    1.43 -
    1.44 -instantiation "fun" :: ("type", "type") itself
    1.45 -begin
    1.46 -
    1.47 -definition "itself = TYPE('a \<Rightarrow> 'b)"
    1.48 -
    1.49 -instance ..
    1.50 -
    1.51 -end
    1.52 -
    1.53 -hide (open) const itself
    1.54 -
    1.55 -end