src/HOL/Nominal/Nominal.thy
changeset 59940 087d81f5213e
parent 58372 bfd497f2f4c2
child 60580 7e741e22d7fc
     1.1 --- a/src/HOL/Nominal/Nominal.thy	Mon Apr 06 22:11:01 2015 +0200
     1.2 +++ b/src/HOL/Nominal/Nominal.thy	Mon Apr 06 23:14:05 2015 +0200
     1.3 @@ -3563,7 +3563,7 @@
     1.4    (* connectives *)
     1.5    if_eqvt imp_eqvt disj_eqvt conj_eqvt neg_eqvt 
     1.6    true_eqvt false_eqvt
     1.7 -  imp_eqvt [folded induct_implies_def]
     1.8 +  imp_eqvt [folded HOL.induct_implies_def]
     1.9    
    1.10    (* datatypes *)
    1.11    perm_unit.simps