doc-src/AxClass/Group/Product.thy

 
-header {* Syntactic classes *};
+header {* Syntactic classes *}
 
-theory Product = Main:;
+theory Product = Main:
 
 text {*
  \medskip\noindent There is still a feature of Isabelle's type system
  left that we have not yet discussed.  When declaring polymorphic
  constants $c :: \sigma$, the type variables occurring in $\sigma$ may

  $term$ is the universal class of HOL, this is not really a constraint
  at all.
 
  The $product$ class below provides a less degenerate example of
  syntactic type classes.
-*};
+*}
 
 axclass
-  product < "term";
+  product < "term"
 consts
-  product :: "'a::product \\<Rightarrow> 'a \\<Rightarrow> 'a"    (infixl "\\<Otimes>" 70);
+  product :: "'a::product \\<Rightarrow> 'a \\<Rightarrow> 'a"    (infixl "\\<Otimes>" 70)
 
 text {*
  Here class $product$ is defined as subclass of $term$ without any
  additional axioms.  This effects in logical equivalence of $product$
  and $term$, as is reflected by the trivial introduction rule

  arguments restricted to an associated (logically trivial) class $c$.
  Only immediately before \emph{specifying} these constants on a
  certain type $\tau$ do we instantiate $\tau :: c$.
 
  This is done for class $product$ and type $bool$ as follows.
-*};
+*}
 
-instance bool :: product;
-  by intro_classes;
+instance bool :: product
+  by intro_classes
 defs
-  product_bool_def: "x \\<Otimes> y \\<equiv> x \\<and> y";
+  product_bool_def: "x \\<Otimes> y \\<equiv> x \\<and> y"
 
 text {*
  The definition $prod_bool_def$ becomes syntactically well-formed only
  after the arity $bool :: product$ is made known to the type checker.
 

  the system what these ``member functions'' should be.
 
  This style of \texttt{instance} won't make much sense in Isabelle's
  meta-logic, because there is no internal notion of ``providing
  operations'' or even ``names of functions''.
-*};
+*}
 
-end;
+end