# HG changeset patch
# User wenzelm
# Date 1468228510 -7200
# Node ID 7743df69a6b41d253d12a9f381de57ed45a9bfc0
# Parent  c956d995bec62918c94155b595e414e6df8c04da
clarified keywords;

diff -r c956d995bec6 -r 7743df69a6b4 src/Tools/Code_Generator.thy
--- a/src/Tools/Code_Generator.thy	Mon Jul 11 10:43:54 2016 +0200
+++ b/src/Tools/Code_Generator.thy	Mon Jul 11 11:15:10 2016 +0200
@@ -10,8 +10,10 @@
   "print_codeproc" "code_thms" "code_deps" :: diag and
   "export_code" "code_identifier" "code_printing" "code_reserved"
     "code_monad" "code_reflect" :: thy_decl and
-  "datatypes" "functions" "module_name" "file" "checking"
-  "constant" "type_constructor" "type_class" "class_relation" "class_instance" "code_module"
+  "checking" and
+  "datatypes" "functions" "module_name" "file"
+    "constant" "type_constructor" "type_class" "class_relation" "class_instance" "code_module"
+    :: quasi_command
 begin
 
 ML_file "~~/src/Tools/cache_io.ML"
diff -r c956d995bec6 -r 7743df69a6b4 src/ZF/Inductive_ZF.thy
--- a/src/ZF/Inductive_ZF.thy	Mon Jul 11 10:43:54 2016 +0200
+++ b/src/ZF/Inductive_ZF.thy	Mon Jul 11 11:15:10 2016 +0200
@@ -16,7 +16,7 @@
 keywords
   "inductive" "coinductive" "inductive_cases" "rep_datatype" "primrec" :: thy_decl and
   "domains" "intros" "monos" "con_defs" "type_intros" "type_elims"
-  "elimination" "induction" "case_eqns" "recursor_eqns"
+    "elimination" "induction" "case_eqns" "recursor_eqns" :: quasi_command
 begin
 
 lemma def_swap_iff: "a == b ==> a = c \<longleftrightarrow> c = b"