src/HOL/Transfer.thy
changeset 56677 660ffb526069
parent 56654 54326fa7afe6
child 57260 8747af0d1012
     1.1 --- a/src/HOL/Transfer.thy	Wed Apr 23 17:57:56 2014 +0200
     1.2 +++ b/src/HOL/Transfer.thy	Wed Apr 23 17:57:56 2014 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  imports Hilbert_Choice BNF_FP_Base Metis Option
     1.5  begin
     1.6  
     1.7 -(* We include Option here altough it's not needed here. 
     1.8 +(* We include Option here although it's not needed here. 
     1.9     By doing this, we avoid a diamond problem for BNF and 
    1.10     FP sugar interpretation defined in this file. *)
    1.11  
    1.12 @@ -238,6 +238,9 @@
    1.13    shows "x = y"
    1.14  using assms by (simp add: eq_onp_def)
    1.15  
    1.16 +lemma eq_onp_top_eq_eq: "eq_onp top = op=" 
    1.17 +by (simp add: eq_onp_def)
    1.18 +
    1.19  lemma eq_onp_same_args:
    1.20    shows "eq_onp P x x = P x"
    1.21  using assms by (auto simp add: eq_onp_def)