author wenzelm Thu Jan 01 17:47:12 2009 +0100 (2009-01-01) changeset 29291 d3cc5398bad5 parent 29290 8fb767245822 child 29292 11045b88af1a
avoid implicit use of prems;
```     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
```