undid 6d7b7a037e8d
authornipkow
Tue Apr 28 19:09:28 2015 +0200 (2015-04-28)
changeset 601519023d59acce6
parent 60150 bd773c47ad0b
child 60152 7b051a6c9e28
undid 6d7b7a037e8d
src/HOL/Extraction.thy
src/HOL/HOL.thy
src/HOL/Hoare_Parallel/OG_Examples.thy
     1.1 --- a/src/HOL/Extraction.thy	Tue Apr 28 16:23:38 2015 +0100
     1.2 +++ b/src/HOL/Extraction.thy	Tue Apr 28 19:09:28 2015 +0200
     1.3 @@ -32,7 +32,7 @@
     1.4    induct_atomize induct_atomize' induct_rulify induct_rulify'
     1.5    induct_rulify_fallback induct_trueI
     1.6    True_implies_equals implies_True_equals TrueE
     1.7 -  False_implies_equals implies_False_swap
     1.8 +  False_implies_equals
     1.9  
    1.10  lemmas [extraction_expand_def] =
    1.11    HOL.induct_forall_def HOL.induct_implies_def HOL.induct_equal_def HOL.induct_conj_def
     2.1 --- a/src/HOL/HOL.thy	Tue Apr 28 16:23:38 2015 +0100
     2.2 +++ b/src/HOL/HOL.thy	Tue Apr 28 19:09:28 2015 +0200
     2.3 @@ -1270,10 +1270,6 @@
     2.4  lemma False_implies_equals: "(False \<Longrightarrow> P) \<equiv> Trueprop True"
     2.5  by default simp_all
     2.6  
     2.7 -lemma implies_False_swap:
     2.8 -  "(False \<Longrightarrow> PROP P \<Longrightarrow> PROP Q) \<equiv> (PROP P \<Longrightarrow> False \<Longrightarrow> PROP Q)"
     2.9 -by(rule swap_prems_eq)
    2.10 -
    2.11  lemma ex_simps:
    2.12    "!!P Q. (EX x. P x & Q)   = ((EX x. P x) & Q)"
    2.13    "!!P Q. (EX x. P & Q x)   = (P & (EX x. Q x))"
    2.14 @@ -1297,7 +1293,7 @@
    2.15  lemmas [simp] =
    2.16    triv_forall_equality (*prunes params*)
    2.17    True_implies_equals implies_True_equals (*prune True in asms*)
    2.18 -  False_implies_equals implies_False_swap (*prune False in asms*)
    2.19 +  False_implies_equals (*prune False in asms*)
    2.20    if_True
    2.21    if_False
    2.22    if_cancel
     3.1 --- a/src/HOL/Hoare_Parallel/OG_Examples.thy	Tue Apr 28 16:23:38 2015 +0100
     3.2 +++ b/src/HOL/Hoare_Parallel/OG_Examples.thy	Tue Apr 28 19:09:28 2015 +0200
     3.3 @@ -192,7 +192,6 @@
     3.4  --\<open>6 subgoals left\<close>
     3.5  prefer 6
     3.6  apply(erule_tac x=i in allE)
     3.7 -apply simp
     3.8  apply fastforce
     3.9  --\<open>5 subgoals left\<close>
    3.10  prefer 5