# HG changeset patch # User Christian Urban # 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"