# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1256427064 -7200
# Node ID f3c192574d2a5334981933be2e74dcb971706317
# Parent  6acf9e001038e670b0439473f3cf52eb2b76794a
added "print_quotients" command to th ekeyword file

diff -r 6acf9e001038 -r f3c192574d2a IntEx.thy
--- a/IntEx.thy	Sun Oct 25 01:15:03 2009 +0200
+++ b/IntEx.thy	Sun Oct 25 01:31:04 2009 +0200
@@ -12,6 +12,8 @@
   apply(auto simp add: mem_def expand_fun_eq)
   done
 
+print_quotients
+
 typ my_int
 
 local_setup {*
diff -r 6acf9e001038 -r f3c192574d2a isar-keywords-prove.el
--- a/isar-keywords-prove.el	Sun Oct 25 01:15:03 2009 +0200
+++ b/isar-keywords-prove.el	Sun Oct 25 01:31:04 2009 +0200
@@ -1,6 +1,6 @@
 ;;
 ;; Keyword classification tables for Isabelle/Isar.
-;; Generated from Pure + HOL + Pure-ProofGeneral + HOL-Nominal-Prove.
+;; Generated from Pure + HOL + Pure-ProofGeneral + HOL-Nominal-test.
 ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
 ;;
 
@@ -161,10 +161,12 @@
     "print_drafts"
     "print_facts"
     "print_induct_rules"
+    "print_interps"
     "print_locale"
     "print_locales"
     "print_methods"
     "print_orders"
+    "print_quotients"
     "print_rules"
     "print_simpset"
     "print_statement"
@@ -344,10 +346,12 @@
     "print_drafts"
     "print_facts"
     "print_induct_rules"
+    "print_interps"
     "print_locale"
     "print_locales"
     "print_methods"
     "print_orders"
+    "print_quotients"
     "print_rules"
     "print_simpset"
     "print_statement"