src/HOL/simpdata.ML
changeset 7648 8258b93cdd32
parent 7623 23efbb7ab889
child 7711 4dae7a4fceaf
     1.1 --- a/src/HOL/simpdata.ML	Wed Sep 29 14:36:36 1999 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Wed Sep 29 14:38:03 1999 +0200
     1.3 @@ -161,7 +161,7 @@
     1.4          (fn _=> [(Blast_tac 1)]) RS mp RS mp);
     1.5  
     1.6  (*Miniscoping: pushing in existential quantifiers*)
     1.7 -val ex_simps = map prover 
     1.8 +val ex_simps = map prover
     1.9                  ["(EX x. P x & Q)   = ((EX x. P x) & Q)",
    1.10                   "(EX x. P & Q x)   = (P & (EX x. Q x))",
    1.11                   "(EX x. P x | Q)   = ((EX x. P x) | Q)",
    1.12 @@ -192,6 +192,10 @@
    1.13  
    1.14  end;
    1.15  
    1.16 +bind_thms ("ex_simps", ex_simps);
    1.17 +bind_thms ("all_simps", all_simps);
    1.18 +
    1.19 +
    1.20  (* Elimination of True from asumptions: *)
    1.21  
    1.22  val True_implies_equals = prove_goal (the_context ())