src/Sequents/LK0.thy
changeset 21588 cd0dc678a205
parent 21524 7843e2fd14a9
child 22894 619b270607ac
equal deleted inserted replaced
21587:a3561bfe0ada 21588:cd0dc678a205
   246 
   246 
   247 end;
   247 end;
   248 *}
   248 *}
   249 
   249 
   250 method_setup fast_prop =
   250 method_setup fast_prop =
   251   {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (fast_tac prop_pack)) *}
   251   {* Method.no_args (Method.SIMPLE_METHOD' (fast_tac prop_pack)) *}
   252   "propositional reasoning"
   252   "propositional reasoning"
   253 
   253 
   254 method_setup fast =
   254 method_setup fast =
   255   {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (fast_tac LK_pack)) *}
   255   {* Method.no_args (Method.SIMPLE_METHOD' (fast_tac LK_pack)) *}
   256   "classical reasoning"
   256   "classical reasoning"
   257 
   257 
   258 method_setup fast_dup =
   258 method_setup fast_dup =
   259   {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (fast_tac LK_dup_pack)) *}
   259   {* Method.no_args (Method.SIMPLE_METHOD' (fast_tac LK_dup_pack)) *}
   260   "classical reasoning"
   260   "classical reasoning"
   261 
   261 
   262 method_setup best =
   262 method_setup best =
   263   {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (best_tac LK_pack)) *}
   263   {* Method.no_args (Method.SIMPLE_METHOD' (best_tac LK_pack)) *}
   264   "classical reasoning"
   264   "classical reasoning"
   265 
   265 
   266 method_setup best_dup =
   266 method_setup best_dup =
   267   {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (best_tac LK_dup_pack)) *}
   267   {* Method.no_args (Method.SIMPLE_METHOD' (best_tac LK_dup_pack)) *}
   268   "classical reasoning"
   268   "classical reasoning"
   269 
   269 
   270 
   270 
   271 lemma mp_R:
   271 lemma mp_R:
   272   assumes major: "$H |- $E, $F, P --> Q"
   272   assumes major: "$H |- $E, $F, P --> Q"