src/HOLCF/Tools/Domain/domain_axioms.ML
changeset 35499 6acef0aea07d
parent 35497 979706bd5c16
child 35513 89eddccbb93d
equal deleted inserted replaced
35498:5c70de748522 35499:6acef0aea07d
   152         let
   152         let
   153           val dnam : string = Long_Name.base_name dname;
   153           val dnam : string = Long_Name.base_name dname;
   154           val take_const = %%:(dname^"_take");
   154           val take_const = %%:(dname^"_take");
   155           val lub = %%: @{const_name lub};
   155           val lub = %%: @{const_name lub};
   156           val image = %%: @{const_name image};
   156           val image = %%: @{const_name image};
   157           val UNIV = %%: @{const_name UNIV};
   157           val UNIV = @{term "UNIV :: nat set"};
   158           val lhs = lub $ (image $ take_const $ UNIV);
   158           val lhs = lub $ (image $ take_const $ UNIV);
   159           val ax = mk_trp (lhs === ID);
   159           val ax = mk_trp (lhs === ID);
   160         in
   160         in
   161           add_one (dnam, [("lub_take", ax)], [])
   161           add_one (dnam, [("lub_take", ax)], [])
   162         end
   162         end