equal
deleted
inserted
replaced
117 |
117 |
118 definition |
118 definition |
119 remember_init_state :: "state assn" ("\<doteq>") |
119 remember_init_state :: "state assn" ("\<doteq>") |
120 where "\<doteq> \<equiv> \<lambda>Y s Z. s = Z" |
120 where "\<doteq> \<equiv> \<lambda>Y s Z. s = Z" |
121 |
121 |
122 lemma remember_init_state_def2 [simp]: "\<doteq> Y = op =" |
122 lemma remember_init_state_def2 [simp]: "\<doteq> Y = (=)" |
123 apply (unfold remember_init_state_def) |
123 apply (unfold remember_init_state_def) |
124 apply (simp (no_asm)) |
124 apply (simp (no_asm)) |
125 done |
125 done |
126 |
126 |
127 definition |
127 definition |