src/HOL/Nominal/nominal_atoms.ML
changeset 44689 f247fc952f31
parent 44684 8dde3352d5c4
child 45133 2214ba5bdfff
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Sat Sep 03 23:38:06 2011 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Sat Sep 03 23:59:36 2011 +0200
     1.3 @@ -747,9 +747,9 @@
     1.4           |> discrete_pt_inst @{type_name nat} @{thm perm_nat_def}
     1.5           |> discrete_fs_inst @{type_name nat} @{thm perm_nat_def}
     1.6           |> discrete_cp_inst @{type_name nat} @{thm perm_nat_def}
     1.7 -         |> discrete_pt_inst @{type_name bool} @{thm perm_bool}
     1.8 -         |> discrete_fs_inst @{type_name bool} @{thm perm_bool}
     1.9 -         |> discrete_cp_inst @{type_name bool} @{thm perm_bool}
    1.10 +         |> discrete_pt_inst @{type_name bool} @{thm perm_bool_def}
    1.11 +         |> discrete_fs_inst @{type_name bool} @{thm perm_bool_def}
    1.12 +         |> discrete_cp_inst @{type_name bool} @{thm perm_bool_def}
    1.13           |> discrete_pt_inst @{type_name int} @{thm perm_int_def}
    1.14           |> discrete_fs_inst @{type_name int} @{thm perm_int_def}
    1.15           |> discrete_cp_inst @{type_name int} @{thm perm_int_def}