src/HOL/Typedef.thy
changeset 11659 a68f930bafb2
parent 11654 53d18ab990f6
child 11743 b9739c85dd44
     1.1 --- a/src/HOL/Typedef.thy	Wed Oct 03 21:01:53 2001 +0200
     1.2 +++ b/src/HOL/Typedef.thy	Wed Oct 03 21:03:05 2001 +0200
     1.3 @@ -6,8 +6,7 @@
     1.4  *)
     1.5  
     1.6  theory Typedef = Set
     1.7 -files "subset.ML" "equalities.ML" "mono.ML"
     1.8 -  "Tools/induct_attrib.ML" ("Tools/typedef_package.ML"):
     1.9 +files "subset.ML" "equalities.ML" "mono.ML" ("Tools/typedef_package.ML"):
    1.10  
    1.11  (* Courtesy of Stephan Merz *)
    1.12  lemma Least_mono: 
    1.13 @@ -128,7 +127,6 @@
    1.14    ultimately show "P x" by (simp only:)
    1.15  qed
    1.16  
    1.17 -setup InductAttrib.setup
    1.18  use "Tools/typedef_package.ML"
    1.19  
    1.20  end