src/HOL/simpdata.ML
changeset 11220 db536a42dfc5
parent 11200 f43fa07536c0
child 11232 558a4feebb04
equal deleted inserted replaced
11219:c4c210e7c89c 11220:db536a42dfc5
   282   val allI = allI
   282   val allI = allI
   283   val allE = allE
   283   val allE = allE
   284 end);
   284 end);
   285 
   285 
   286 local
   286 local
   287 val ex_pattern =
   287 val ex_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))
   288   Thm.read_cterm (Theory.sign_of (the_context ())) ("EX x. P(x) & Q(x)",HOLogic.boolT)
   288     ("EX x. P(x) & Q(x)",HOLogic.boolT)
   289 
   289 val all_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))
   290 val all_pattern =
   290     ("ALL x. P(x) & P'(x) --> Q(x)",HOLogic.boolT)
   291   Thm.read_cterm (Theory.sign_of (the_context ())) ("ALL x. P(x) & P'(x) --> Q(x)",HOLogic.boolT)
       
   292 
       
   293 in
   291 in
   294 val defEX_regroup =
   292 val defEX_regroup = mk_simproc "defined EX" [ex_pattern]
   295   mk_simproc "defined EX" [ex_pattern] Quantifier1.rearrange_ex;
   293       Quantifier1.rearrange_ex
   296 val defALL_regroup =
   294 val defALL_regroup = mk_simproc "defined ALL" [all_pattern]
   297   mk_simproc "defined ALL" [all_pattern] Quantifier1.rearrange_all;
   295       Quantifier1.rearrange_all
   298 end;
   296 end;
   299 
   297 
   300 
   298 
   301 (*** Case splitting ***)
   299 (*** Case splitting ***)
   302 
   300