src/HOL/Partial_Function.thy
changeset 64634 5bd30359e46e
parent 63561 fba08009ff3e
child 66364 fa3247e6ee4b
     1.1 --- a/src/HOL/Partial_Function.thy	Wed Dec 21 21:26:26 2016 +0100
     1.2 +++ b/src/HOL/Partial_Function.thy	Thu Dec 22 08:43:30 2016 +0100
     1.3 @@ -283,8 +283,8 @@
     1.4  lemma flat_ord_antisym: "\<lbrakk> flat_ord a x y; flat_ord a y x \<rbrakk> \<Longrightarrow> x = y"
     1.5  by(auto simp add: flat_ord_def)
     1.6  
     1.7 -lemma antisymP_flat_ord: "antisymP (flat_ord a)"
     1.8 -by(rule antisymI)(auto dest: flat_ord_antisym)
     1.9 +lemma antisymp_flat_ord: "antisymp (flat_ord a)"
    1.10 +by(rule antisympI)(auto dest: flat_ord_antisym)
    1.11  
    1.12  interpretation tailrec:
    1.13    partial_function_definitions "flat_ord undefined" "flat_lub undefined"