--- a/src/HOL/HahnBanach/FunctionNorm.thy Thu Jan 01 14:23:39 2009 +0100
+++ b/src/HOL/HahnBanach/FunctionNorm.thy Thu Jan 01 17:47:12 2009 +0100
@@ -204,7 +204,7 @@
shows "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>"
proof -
interpret continuous V norm f by fact
- interpret linearform V f .
+ interpret linearform V f by fact
show ?thesis
proof cases
assume "x = 0"
--- a/src/HOL/HahnBanach/HahnBanach.thy Thu Jan 01 14:23:39 2009 +0100
+++ b/src/HOL/HahnBanach/HahnBanach.thy Thu Jan 01 17:47:12 2009 +0100
@@ -492,7 +492,7 @@
then have "\<bar>f x\<bar> = \<bar>g x\<bar>" by (simp only:)
also from g_cont
have "\<dots> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>"
- proof (rule fn_norm_le_cong [of g, folded B_def fn_norm_def])
+ proof (rule fn_norm_le_cong [OF _ linearformE, folded B_def fn_norm_def])
from FE x show "x \<in> E" ..
qed
finally show "\<bar>f x\<bar> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>" .
--- a/src/HOL/Statespace/DistinctTreeProver.thy Thu Jan 01 14:23:39 2009 +0100
+++ b/src/HOL/Statespace/DistinctTreeProver.thy Thu Jan 01 17:47:12 2009 +0100
@@ -452,7 +452,7 @@
case Tip thus ?case by simp
next
case (Node l x d r)
- have sub: "subtract (Node l x d r) t\<^isub>2 = Some t".
+ have sub: "subtract (Node l x d r) t\<^isub>2 = Some t" by fact
show ?case
proof (cases "delete x t\<^isub>2")
case (Some t\<^isub>2')
--- a/src/HOL/Statespace/state_space.ML Thu Jan 01 14:23:39 2009 +0100
+++ b/src/HOL/Statespace/state_space.ML Thu Jan 01 17:47:12 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Statespace/state_space.ML
- ID: $Id$
Author: Norbert Schirmer, TU Muenchen
*)
@@ -421,7 +420,10 @@
val expr = ([(suffix valuetypesN name,
(("",false),Expression.Positional (map SOME pars)))],[]);
- in prove_interpretation_in (K all_tac) (suffix valuetypesN name, expr) thy end;
+ in
+ prove_interpretation_in (ALLGOALS o solve_tac o Assumption.prems_of)
+ (suffix valuetypesN name, expr) thy
+ end;
fun interprete_parent (_, pname, rs) =
let