src/HOL/TLA/Init.thy
changeset 26304 02fbd0e7954a
parent 21624 6f79647cf536
child 35108 e384e27c229f
     1.1 --- a/src/HOL/TLA/Init.thy	Mon Mar 17 18:37:04 2008 +0100
     1.2 +++ b/src/HOL/TLA/Init.thy	Mon Mar 17 18:37:05 2008 +0100
     1.3 @@ -45,7 +45,7 @@
     1.4    "|- (Init #False) = #False"
     1.5    by (auto simp: Init_def)
     1.6  
     1.7 -lemma Init_simps [int_rewrite]:
     1.8 +lemma Init_simps1 [int_rewrite]:
     1.9    "!!F. |- (Init ~F) = (~ Init F)"
    1.10    "|- (Init (P --> Q)) = (Init P --> Init Q)"
    1.11    "|- (Init (P & Q)) = (Init P & Init Q)"
    1.12 @@ -59,13 +59,13 @@
    1.13  lemma Init_stp_act: "|- (Init $P) = (Init P)"
    1.14    by (auto simp add: Init_def fw_act_def fw_stp_def)
    1.15  
    1.16 -lemmas Init_simps = Init_stp_act [int_rewrite] Init_simps
    1.17 +lemmas Init_simps2 = Init_stp_act [int_rewrite] Init_simps1
    1.18  lemmas Init_stp_act_rev = Init_stp_act [int_rewrite, symmetric]
    1.19  
    1.20  lemma Init_temp: "|- (Init F) = F"
    1.21    by (auto simp add: Init_def fw_temp_def)
    1.22  
    1.23 -lemmas Init_simps = Init_temp [int_rewrite] Init_simps
    1.24 +lemmas Init_simps = Init_temp [int_rewrite] Init_simps2
    1.25  
    1.26  (* Trivial instances of the definitions that avoid introducing lambda expressions. *)
    1.27  lemma Init_stp: "(sigma |= Init P) = P (st1 sigma)"