src/HOL/simpdata.ML
changeset 11220 db536a42dfc5
parent 11200 f43fa07536c0
child 11232 558a4feebb04
     1.1 --- a/src/HOL/simpdata.ML	Thu Mar 22 10:29:26 2001 +0100
     1.2 +++ b/src/HOL/simpdata.ML	Fri Mar 23 10:10:53 2001 +0100
     1.3 @@ -284,17 +284,15 @@
     1.4  end);
     1.5  
     1.6  local
     1.7 -val ex_pattern =
     1.8 -  Thm.read_cterm (Theory.sign_of (the_context ())) ("EX x. P(x) & Q(x)",HOLogic.boolT)
     1.9 -
    1.10 -val all_pattern =
    1.11 -  Thm.read_cterm (Theory.sign_of (the_context ())) ("ALL x. P(x) & P'(x) --> Q(x)",HOLogic.boolT)
    1.12 -
    1.13 +val ex_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))
    1.14 +    ("EX x. P(x) & Q(x)",HOLogic.boolT)
    1.15 +val all_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))
    1.16 +    ("ALL x. P(x) & P'(x) --> Q(x)",HOLogic.boolT)
    1.17  in
    1.18 -val defEX_regroup =
    1.19 -  mk_simproc "defined EX" [ex_pattern] Quantifier1.rearrange_ex;
    1.20 -val defALL_regroup =
    1.21 -  mk_simproc "defined ALL" [all_pattern] Quantifier1.rearrange_all;
    1.22 +val defEX_regroup = mk_simproc "defined EX" [ex_pattern]
    1.23 +      Quantifier1.rearrange_ex
    1.24 +val defALL_regroup = mk_simproc "defined ALL" [all_pattern]
    1.25 +      Quantifier1.rearrange_all
    1.26  end;
    1.27  
    1.28