Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
added "print_quotients" command to th ekeyword file
authorChristian Urban <urbanc@in.tum.de>
Sun, 25 Oct 2009 01:31:04 +0200
changeset 184 f3c192574d2a
parent 183 6acf9e001038
child 185 929bc55efff7
added "print_quotients" command to th ekeyword file
IntEx.thy file | annotate | diff | comparison | revisions
isar-keywords-prove.el file | annotate | diff | comparison | revisions 
--- 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 {*
--- 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"
nominal2