src/HOL/FunDef.thy
changeset 21211 5370cfbf3070
parent 21051 c49467a9c1e1
child 21312 1d39091a3208
     1.1 --- a/src/HOL/FunDef.thy	Tue Nov 07 11:47:57 2006 +0100
     1.2 +++ b/src/HOL/FunDef.thy	Tue Nov 07 11:53:55 2006 +0100
     1.3 @@ -189,11 +189,6 @@
     1.4    "rproj (Inr x) = x"
     1.5    by (auto simp:rproj_def intro: the_equality rpg.intros elim: rpg.cases)
     1.6  
     1.7 -
     1.8 -
     1.9 -lemma P_imp_P: "P \<Longrightarrow> P" .
    1.10 -
    1.11 -
    1.12  use "Tools/function_package/sum_tools.ML"
    1.13  use "Tools/function_package/fundef_common.ML"
    1.14  use "Tools/function_package/fundef_lib.ML"
    1.15 @@ -205,16 +200,11 @@
    1.16  use "Tools/function_package/mutual.ML"
    1.17  use "Tools/function_package/pattern_split.ML"
    1.18  use "Tools/function_package/fundef_package.ML"
    1.19 +use "Tools/function_package/auto_term.ML"
    1.20  
    1.21  setup FundefPackage.setup
    1.22 -
    1.23 -use "Tools/function_package/fundef_datatype.ML"
    1.24 -setup FundefDatatype.setup
    1.25 -
    1.26 -use "Tools/function_package/auto_term.ML"
    1.27  setup FundefAutoTerm.setup
    1.28  
    1.29 -
    1.30  lemmas [fundef_cong] = 
    1.31    let_cong if_cong image_cong INT_cong UN_cong bex_cong ball_cong imp_cong
    1.32