more porting to new datatypes
authorblanchet
Tue Sep 09 20:51:36 2014 +0200 (2014-09-09)
changeset 5827016648edf16e3
parent 58269 ad644790cbbb
child 58271 2e91e9bbc212
more porting to new datatypes
src/HOL/HOLCF/IOA/NTP/Correctness.thy
src/HOL/HOLCF/IOA/NTP/Impl.thy
src/HOL/HOLCF/IOA/Storage/Correctness.thy
src/HOL/Induct/Common_Patterns.thy
     1.1 --- a/src/HOL/HOLCF/IOA/NTP/Correctness.thy	Tue Sep 09 20:51:36 2014 +0200
     1.2 +++ b/src/HOL/HOLCF/IOA/NTP/Correctness.thy	Tue Sep 09 20:51:36 2014 +0200
     1.3 @@ -89,7 +89,7 @@
     1.4  apply (simp add: hom_ioas)
     1.5  apply (blast dest!: add_leD1 [THEN leD])
     1.6  
     1.7 -apply (case_tac "m = hd (sq (sen (s)))")
     1.8 +apply (rename_tac m, case_tac "m = hd (sq (sen (s)))")
     1.9  
    1.10  apply force
    1.11  
     2.1 --- a/src/HOL/HOLCF/IOA/NTP/Impl.thy	Tue Sep 09 20:51:36 2014 +0200
     2.2 +++ b/src/HOL/HOLCF/IOA/NTP/Impl.thy	Tue Sep 09 20:51:36 2014 +0200
     2.3 @@ -347,7 +347,7 @@
     2.4    apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv3_def}]
     2.5                                 (@{thm raw_inv3} RS @{thm invariantE})] 1 *})
     2.6    apply simp
     2.7 -  apply (erule_tac x = "m" in allE)
     2.8 +  apply (rename_tac m, erule_tac x = "m" in allE)
     2.9    apply simp
    2.10    done
    2.11  
     3.1 --- a/src/HOL/HOLCF/IOA/Storage/Correctness.thy	Tue Sep 09 20:51:36 2014 +0200
     3.2 +++ b/src/HOL/HOLCF/IOA/Storage/Correctness.thy	Tue Sep 09 20:51:36 2014 +0200
     3.3 @@ -53,7 +53,7 @@
     3.4  apply (simp (no_asm) add: spec_ioa_def spec_trans_def trans_of_def)
     3.5  apply fast
     3.6  txt {* FREE *}
     3.7 -apply (rule_tac x = " (used - {nat},c) " in exI)
     3.8 +apply (rename_tac nat, rule_tac x = " (used - {nat},c) " in exI)
     3.9  apply simp
    3.10  apply (rule transition_is_ex)
    3.11  apply (simp (no_asm) add: spec_ioa_def spec_trans_def trans_of_def)
     4.1 --- a/src/HOL/Induct/Common_Patterns.thy	Tue Sep 09 20:51:36 2014 +0200
     4.2 +++ b/src/HOL/Induct/Common_Patterns.thy	Tue Sep 09 20:51:36 2014 +0200
     4.3 @@ -224,7 +224,7 @@
     4.4  
     4.5  text {*
     4.6    The pack of induction rules for this datatype is: @{thm [display]
     4.7 -  foo_bar_bazar.inducts [no_vars]}
     4.8 +  foo.induct [no_vars] bar.induct [no_vars] bazar.induct [no_vars]}
     4.9  
    4.10    This corresponds to the following basic proof pattern:
    4.11  *}