avoid implicit use of prems;
authorwenzelm
Thu Jan 01 17:47:12 2009 +0100 (2009-01-01)
changeset 29291d3cc5398bad5
parent 29290 8fb767245822
child 29292 11045b88af1a
avoid implicit use of prems;
src/HOL/HahnBanach/FunctionNorm.thy
src/HOL/HahnBanach/HahnBanach.thy
src/HOL/Statespace/DistinctTreeProver.thy
src/HOL/Statespace/state_space.ML
     1.1 --- a/src/HOL/HahnBanach/FunctionNorm.thy	Thu Jan 01 14:23:39 2009 +0100
     1.2 +++ b/src/HOL/HahnBanach/FunctionNorm.thy	Thu Jan 01 17:47:12 2009 +0100
     1.3 @@ -204,7 +204,7 @@
     1.4    shows "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>"
     1.5  proof -
     1.6    interpret continuous V norm f by fact
     1.7 -  interpret linearform V f .
     1.8 +  interpret linearform V f by fact
     1.9    show ?thesis
    1.10    proof cases
    1.11      assume "x = 0"
     2.1 --- a/src/HOL/HahnBanach/HahnBanach.thy	Thu Jan 01 14:23:39 2009 +0100
     2.2 +++ b/src/HOL/HahnBanach/HahnBanach.thy	Thu Jan 01 17:47:12 2009 +0100
     2.3 @@ -492,7 +492,7 @@
     2.4  	then have "\<bar>f x\<bar> = \<bar>g x\<bar>" by (simp only:)
     2.5  	also from g_cont
     2.6  	have "\<dots> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>"
     2.7 -	proof (rule fn_norm_le_cong [of g, folded B_def fn_norm_def])
     2.8 +	proof (rule fn_norm_le_cong [OF _ linearformE, folded B_def fn_norm_def])
     2.9  	  from FE x show "x \<in> E" ..
    2.10  	qed
    2.11  	finally show "\<bar>f x\<bar> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>" .
     3.1 --- a/src/HOL/Statespace/DistinctTreeProver.thy	Thu Jan 01 14:23:39 2009 +0100
     3.2 +++ b/src/HOL/Statespace/DistinctTreeProver.thy	Thu Jan 01 17:47:12 2009 +0100
     3.3 @@ -452,7 +452,7 @@
     3.4    case Tip thus ?case by simp
     3.5  next
     3.6    case (Node l x d r)
     3.7 -  have sub: "subtract (Node l x d r) t\<^isub>2 = Some t".
     3.8 +  have sub: "subtract (Node l x d r) t\<^isub>2 = Some t" by fact
     3.9    show ?case
    3.10    proof (cases "delete x t\<^isub>2")
    3.11      case (Some t\<^isub>2')
     4.1 --- a/src/HOL/Statespace/state_space.ML	Thu Jan 01 14:23:39 2009 +0100
     4.2 +++ b/src/HOL/Statespace/state_space.ML	Thu Jan 01 17:47:12 2009 +0100
     4.3 @@ -1,5 +1,4 @@
     4.4  (*  Title:      HOL/Statespace/state_space.ML
     4.5 -    ID:         $Id$
     4.6      Author:     Norbert Schirmer, TU Muenchen
     4.7  *)
     4.8  
     4.9 @@ -421,7 +420,10 @@
    4.10  
    4.11          val expr = ([(suffix valuetypesN name, 
    4.12                       (("",false),Expression.Positional (map SOME pars)))],[]);
    4.13 -      in prove_interpretation_in (K all_tac) (suffix valuetypesN name, expr) thy end;
    4.14 +      in
    4.15 +        prove_interpretation_in (ALLGOALS o solve_tac o Assumption.prems_of)
    4.16 +          (suffix valuetypesN name, expr) thy
    4.17 +      end;
    4.18  
    4.19      fun interprete_parent (_, pname, rs) =
    4.20        let