equal
deleted
inserted
replaced
888 \emph{subtypes} of the generic atom type that only include atoms of a single |
888 \emph{subtypes} of the generic atom type that only include atoms of a single |
889 specific sort. We call such subtypes \emph{concrete atom types}. |
889 specific sort. We call such subtypes \emph{concrete atom types}. |
890 |
890 |
891 The following Isabelle/HOL command defines a concrete atom type called |
891 The following Isabelle/HOL command defines a concrete atom type called |
892 \emph{name}, which consists of atoms whose sort equals the string @{term |
892 \emph{name}, which consists of atoms whose sort equals the string @{term |
893 "''name''"}. |
893 "''Thy.name''"}. |
894 |
894 |
895 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
895 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
896 \isacommand{typedef}\ \ @{typ name} = @{term "{a. sort\<iota> a = ''name''}"} |
896 \isacommand{typedef}\ \ @{typ name} = @{term "{a. sort\<iota> a = ''Thy.name''}"} |
897 \end{isabelle} |
897 \end{isabelle} |
898 |
898 |
899 \noindent |
899 \noindent |
900 This command automatically generates injective functions that map from the |
900 This command automatically generates injective functions that map from the |
901 concrete atom type into the generic atom type and back, called |
901 concrete atom type into the generic atom type and back, called |