src/HOL/Multivariate_Analysis/normarith.ML
changeset 60801 7664e0916eec
parent 60754 02924903a6fd
child 60949 ccbf9379e355
     1.1 --- a/src/HOL/Multivariate_Analysis/normarith.ML	Mon Jul 27 16:35:12 2015 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/normarith.ML	Mon Jul 27 17:44:55 2015 +0200
     1.3 @@ -154,7 +154,7 @@
     1.4          (Numeral.mk_cnumber @{ctyp "real"} b)
     1.5  end;
     1.6  
     1.7 -fun norm_cmul_rule c th = instantiate' [] [SOME (cterm_of_rat c)] (th RS @{thm norm_cmul_rule_thm});
     1.8 +fun norm_cmul_rule c th = Thm.instantiate' [] [SOME (cterm_of_rat c)] (th RS @{thm norm_cmul_rule_thm});
     1.9  
    1.10  fun norm_add_rule th1 th2 = [th1, th2] MRS @{thm norm_add_rule_thm};
    1.11  
    1.12 @@ -342,7 +342,7 @@
    1.13    val ntms = fold_rev find_normedterms (map (Thm.dest_arg o concl) (ges @ gts)) []
    1.14    val lctab = vector_lincombs (map snd (filter (not o fst) ntms))
    1.15    val (fxns, ctxt') = Variable.variant_fixes (replicate (length lctab) "x") ctxt
    1.16 -  fun instantiate_cterm' ty tms = Drule.cterm_rule (Drule.instantiate' ty tms)
    1.17 +  fun instantiate_cterm' ty tms = Drule.cterm_rule (Thm.instantiate' ty tms)
    1.18    fun mk_norm t = Thm.apply (instantiate_cterm' [SOME (Thm.ctyp_of_cterm t)] [] @{cpat "norm :: (?'a :: real_normed_vector) => real"}) t
    1.19    fun mk_equals l r = Thm.apply (Thm.apply (instantiate_cterm' [SOME (Thm.ctyp_of_cterm l)] [] @{cpat "op == :: ?'a =>_"}) l) r
    1.20    val asl = map2 (fn (t,_) => fn n => Thm.assume (mk_equals (mk_norm t) (Thm.cterm_of ctxt' (Free(n,@{typ real}))))) lctab fxns