# HG changeset patch # User wenzelm # Date 1230828432 -3600 # Node ID d3cc5398bad5f42e42afda3b26ccfbf24bda3e41 # Parent 8fb76724582236d1bb89e27f9498a468e6baa5c7 avoid implicit use of prems; diff -r 8fb767245822 -r d3cc5398bad5 src/HOL/HahnBanach/FunctionNorm.thy --- 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 "\f x\ \ \f\\V * \x\" 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" diff -r 8fb767245822 -r d3cc5398bad5 src/HOL/HahnBanach/HahnBanach.thy --- 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 "\f x\ = \g x\" by (simp only:) also from g_cont have "\ \ \g\\E * \x\" - 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 \ E" .. qed finally show "\f x\ \ \g\\E * \x\" . diff -r 8fb767245822 -r d3cc5398bad5 src/HOL/Statespace/DistinctTreeProver.thy --- 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') diff -r 8fb767245822 -r d3cc5398bad5 src/HOL/Statespace/state_space.ML --- 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