src/ZF/Inductive_ZF.thy
changeset 38514 bd9c4e8281ec
parent 29580 117b88da143c
child 46821 ff6b0c1087f2
     1.1 --- a/src/ZF/Inductive_ZF.thy	Wed Aug 18 12:08:21 2010 +0200
     1.2 +++ b/src/ZF/Inductive_ZF.thy	Wed Aug 18 12:19:27 2010 +0200
     1.3 @@ -31,8 +31,8 @@
     1.4  lemma refl_thin: "!!P. a = a ==> P ==> P" .
     1.5  
     1.6  use "ind_syntax.ML"
     1.7 +use "Tools/ind_cases.ML"
     1.8  use "Tools/cartprod.ML"
     1.9 -use "Tools/ind_cases.ML"
    1.10  use "Tools/inductive_package.ML"
    1.11  use "Tools/induct_tacs.ML"
    1.12  use "Tools/primrec_package.ML"