src/HOL/Nominal/nominal_atoms.ML
changeset 18579 002d371401f5
parent 18438 b8d867177916
child 18600 20ad06db427b
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Wed Jan 04 20:20:25 2006 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Thu Jan 05 12:09:26 2006 +0100
     1.3 @@ -406,7 +406,7 @@
     1.4  
     1.5       (* show that                       *)
     1.6       (*      fun(pt_<ak>,pt_<ak>)       *)
     1.7 -     (*      nOption(pt_<ak>)           *)
     1.8 +     (*      noption(pt_<ak>)           *)
     1.9       (*      option(pt_<ak>)            *)
    1.10       (*      list(pt_<ak>)              *)
    1.11       (*      *(pt_<ak>,pt_<ak>)         *)
    1.12 @@ -433,7 +433,7 @@
    1.13         in 
    1.14  	thy
    1.15  	|> AxClass.add_inst_arity_i ("fun",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_fun)
    1.16 -        |> AxClass.add_inst_arity_i ("nominal.nOption",[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn) 
    1.17 +        |> AxClass.add_inst_arity_i ("nominal.noption",[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn) 
    1.18          |> AxClass.add_inst_arity_i ("Datatype.option",[[cls_name]],[cls_name]) (pt_proof pt_thm_optn)
    1.19          |> AxClass.add_inst_arity_i ("List.list",[[cls_name]],[cls_name]) (pt_proof pt_thm_list)
    1.20          |> AxClass.add_inst_arity_i ("*",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod)
    1.21 @@ -575,7 +575,7 @@
    1.22           |> AxClass.add_inst_arity_i ("List.list",[[cls_name]],[cls_name]) (cp_proof cp_thm_list)
    1.23           |> AxClass.add_inst_arity_i ("fun",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_fun)
    1.24           |> AxClass.add_inst_arity_i ("Datatype.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn)
    1.25 -         |> AxClass.add_inst_arity_i ("nominal.nOption",[[cls_name]],[cls_name]) (cp_proof cp_thm_noptn)
    1.26 +         |> AxClass.add_inst_arity_i ("nominal.noption",[[cls_name]],[cls_name]) (cp_proof cp_thm_noptn)
    1.27          end) ak_names thy) ak_names thy25;
    1.28         
    1.29       (* show that discrete nominal types are permutation types, finitely     *)