src/HOL/Tools/Function/function_core.ML
changeset 55085 0e8e4dc55866
parent 53603 59ef06cda7b9
child 55396 91bc9f69a958
     1.1 --- a/src/HOL/Tools/Function/function_core.ML	Mon Jan 20 20:42:43 2014 +0100
     1.2 +++ b/src/HOL/Tools/Function/function_core.ML	Mon Jan 20 21:32:41 2014 +0100
     1.3 @@ -81,14 +81,14 @@
     1.4  (* Theory dependencies. *)
     1.5  val acc_induct_rule = @{thm accp_induct_rule}
     1.6  
     1.7 -val ex1_implies_ex = @{thm FunDef.fundef_ex1_existence}
     1.8 -val ex1_implies_un = @{thm FunDef.fundef_ex1_uniqueness}
     1.9 -val ex1_implies_iff = @{thm FunDef.fundef_ex1_iff}
    1.10 +val ex1_implies_ex = @{thm Fun_Def.fundef_ex1_existence}
    1.11 +val ex1_implies_un = @{thm Fun_Def.fundef_ex1_uniqueness}
    1.12 +val ex1_implies_iff = @{thm Fun_Def.fundef_ex1_iff}
    1.13  
    1.14  val acc_downward = @{thm accp_downward}
    1.15  val accI = @{thm accp.accI}
    1.16  val case_split = @{thm HOL.case_split}
    1.17 -val fundef_default_value = @{thm FunDef.fundef_default_value}
    1.18 +val fundef_default_value = @{thm Fun_Def.fundef_default_value}
    1.19  val not_acc_down = @{thm not_accp_down}
    1.20  
    1.21  
    1.22 @@ -494,7 +494,7 @@
    1.23  fun define_function fdefname (fname, mixfix) domT ranT G default lthy =
    1.24    let
    1.25      val f_def =
    1.26 -      Abs ("x", domT, Const (@{const_name FunDef.THE_default}, ranT --> (ranT --> boolT) --> ranT)
    1.27 +      Abs ("x", domT, Const (@{const_name Fun_Def.THE_default}, ranT --> (ranT --> boolT) --> ranT)
    1.28          $ (default $ Bound 0) $ Abs ("y", ranT, G $ Bound 1 $ Bound 0))
    1.29        |> Syntax.check_term lthy
    1.30    in
    1.31 @@ -718,8 +718,8 @@
    1.32  (** Termination rule **)
    1.33  
    1.34  val wf_induct_rule = @{thm Wellfounded.wfP_induct_rule}
    1.35 -val wf_in_rel = @{thm FunDef.wf_in_rel}
    1.36 -val in_rel_def = @{thm FunDef.in_rel_def}
    1.37 +val wf_in_rel = @{thm Fun_Def.wf_in_rel}
    1.38 +val in_rel_def = @{thm Fun_Def.in_rel_def}
    1.39  
    1.40  fun mk_nest_term_case ctxt globals R' ihyp clause =
    1.41    let
    1.42 @@ -780,7 +780,7 @@
    1.43      val R' = Free ("R", fastype_of R)
    1.44  
    1.45      val Rrel = Free ("R", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)))
    1.46 -    val inrel_R = Const (@{const_name FunDef.in_rel},
    1.47 +    val inrel_R = Const (@{const_name Fun_Def.in_rel},
    1.48        HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel
    1.49  
    1.50      val wfR' = HOLogic.mk_Trueprop (Const (@{const_name Wellfounded.wfP},