# HG changeset patch
# User kuncar
# Date 1358167438 -3600
# Node ID a2a1a5907f7ba7988aa99766d956ae4ca41dda70
# Parent  e6317e8b11dbfccb5ec498e95b6b0263331e94b5
update isar-ref for Quotient and Lifting package

diff -r e6317e8b11db -r a2a1a5907f7b src/Doc/IsarRef/HOL_Specific.thy
--- a/src/Doc/IsarRef/HOL_Specific.thy	Mon Jan 14 10:32:33 2013 +0100
+++ b/src/Doc/IsarRef/HOL_Specific.thy	Mon Jan 14 13:43:58 2013 +0100
@@ -1258,7 +1258,7 @@
   corresponding constants and facts on the raw type.
 
   @{rail "
-    @@{command (HOL) quotient_type} (spec + @'and');
+    @@{command (HOL) quotient_type} (spec);
 
     spec: @{syntax typespec} @{syntax mixfix}? '=' \\
      @{syntax type} '/' ('partial' ':')? @{syntax term} \\
@@ -1514,10 +1514,12 @@
     @{command_def (HOL) "print_quotients"} & : & @{text "context \<rightarrow>"}\\
     @{attribute_def (HOL) "quot_map"} & : & @{text attribute} \\
     @{attribute_def (HOL) "invariant_commute"} & : & @{text attribute} \\
+    @{attribute_def (HOL) "reflexivity_rule"} & : & @{text attribute} \\
+    @{attribute_def (HOL) "quot_del"} & : & @{text attribute}
   \end{matharray}
 
   @{rail "
-    @@{command (HOL) setup_lifting} ('(' 'no_abs_code' ')')? \\
+    @@{command (HOL) setup_lifting} ('(' 'no_code' ')')? \\
       @{syntax thmref} @{syntax thmref}?;
   "}
 
@@ -1548,7 +1550,7 @@
     the theorem is declared as an abstract type in the code
     generator. This allows @{command (HOL) "lift_definition"} to
     register (generated) code certificate theorems as abstract code
-    equations in the code generator.  The option @{text "no_abs_code"}
+    equations in the code generator.  The option @{text "no_code"}
     of the command @{command (HOL) "setup_lifting"} can turn off that
     behavior and causes that code certificate theorems generated by
     @{command (HOL) "lift_definition"} are not registred as abstract
@@ -1584,7 +1586,7 @@
     "~~/src/HOL/Library/Quotient_List.thy"} or other Quotient_*.thy
     files.
 
-  \item @{attribute (HOL) invariant_commute} registers a theorem which
+  \item @{attribute (HOL) invariant_commute} registers a theorem that
     shows a relationship between the constant @{text
     Lifting.invariant} (used for internal encoding of proper subtypes)
     and a relator.  Such theorems allows the package to hide @{text
@@ -1593,6 +1595,17 @@
     "~~/src/HOL/Library/Quotient_List.thy"} or other Quotient_*.thy
     files.
 
+  \item @{attribute (HOL) reflexivity_rule} registers a theorem that shows
+    that a relator respects reflexivity and left-totality. For exampless 
+    see @{file "~~/src/HOL/Library/Quotient_List.thy"} or other Quotient_*.thy
+    The property is used in generation of abstraction function equations.
+
+  \item @{attribute (HOL) quot_del} deletes a corresponding Quotient theorem
+    from the Lifting infrastructure and thus de-register the corresponding quotient. 
+    This effectively causes that @{command (HOL) lift_definition}  will not
+    do any lifting for the corresponding type. It serves mainly for hiding
+    of type construction details when the construction is done. See for example
+    @{file "~~/src/HOL/Int.thy"}.
   \end{description}
 *}