1.1 --- a/etc/isar-keywords-ZF.el Mon May 11 09:18:42 2009 +0200
1.2 +++ b/etc/isar-keywords-ZF.el Mon May 11 09:39:53 2009 +0200
1.3 @@ -45,15 +45,18 @@
1.4 "class_deps"
1.5 "classes"
1.6 "classrel"
1.7 + "codatatype"
1.8 "code_datatype"
1.9 "code_library"
1.10 "code_module"
1.11 + "coinductive"
1.12 "commit"
1.13 "constdefs"
1.14 "consts"
1.15 "consts_code"
1.16 "context"
1.17 "corollary"
1.18 + "datatype"
1.19 "declaration"
1.20 "declare"
1.21 "def"
1.22 @@ -83,6 +86,8 @@
1.23 "help"
1.24 "hence"
1.25 "hide"
1.26 + "inductive"
1.27 + "inductive_cases"
1.28 "init_toplevel"
1.29 "instance"
1.30 "instantiation"
1.31 @@ -118,6 +123,7 @@
1.32 "presume"
1.33 "pretty_setmargin"
1.34 "prf"
1.35 + "primrec"
1.36 "print_abbrevs"
1.37 "print_antiquotations"
1.38 "print_ast_translation"
1.39 @@ -140,6 +146,7 @@
1.40 "print_simpset"
1.41 "print_statement"
1.42 "print_syntax"
1.43 + "print_tcset"
1.44 "print_theorems"
1.45 "print_theory"
1.46 "print_trans_rules"
1.47 @@ -154,6 +161,7 @@
1.48 "realizability"
1.49 "realizers"
1.50 "remove_thy"
1.51 + "rep_datatype"
1.52 "sect"
1.53 "section"
1.54 "setup"
1.55 @@ -207,9 +215,13 @@
1.56 "attach"
1.57 "begin"
1.58 "binder"
1.59 + "case_eqns"
1.60 + "con_defs"
1.61 "constrains"
1.62 "contains"
1.63 "defines"
1.64 + "domains"
1.65 + "elimination"
1.66 "file"
1.67 "fixes"
1.68 "for"
1.69 @@ -217,17 +229,23 @@
1.70 "if"
1.71 "imports"
1.72 "in"
1.73 + "induction"
1.74 "infix"
1.75 "infixl"
1.76 "infixr"
1.77 + "intros"
1.78 "is"
1.79 + "monos"
1.80 "notes"
1.81 "obtains"
1.82 "open"
1.83 "output"
1.84 "overloaded"
1.85 + "recursor_eqns"
1.86 "shows"
1.87 "structure"
1.88 + "type_elims"
1.89 + "type_intros"
1.90 "unchecked"
1.91 "uses"
1.92 "where"))
1.93 @@ -295,6 +313,7 @@
1.94 "print_simpset"
1.95 "print_statement"
1.96 "print_syntax"
1.97 + "print_tcset"
1.98 "print_theorems"
1.99 "print_theory"
1.100 "print_trans_rules"
1.101 @@ -338,13 +357,16 @@
1.102 "class"
1.103 "classes"
1.104 "classrel"
1.105 + "codatatype"
1.106 "code_datatype"
1.107 "code_library"
1.108 "code_module"
1.109 + "coinductive"
1.110 "constdefs"
1.111 "consts"
1.112 "consts_code"
1.113 "context"
1.114 + "datatype"
1.115 "declaration"
1.116 "declare"
1.117 "defaultsort"
1.118 @@ -355,6 +377,7 @@
1.119 "finalconsts"
1.120 "global"
1.121 "hide"
1.122 + "inductive"
1.123 "instantiation"
1.124 "judgment"
1.125 "lemmas"
1.126 @@ -371,11 +394,13 @@
1.127 "overloading"
1.128 "parse_ast_translation"
1.129 "parse_translation"
1.130 + "primrec"
1.131 "print_ast_translation"
1.132 "print_translation"
1.133 "quickcheck_params"
1.134 "realizability"
1.135 "realizers"
1.136 + "rep_datatype"
1.137 "setup"
1.138 "simproc_setup"
1.139 "syntax"
1.140 @@ -390,7 +415,7 @@
1.141 "use"))
1.142
1.143 (defconst isar-keywords-theory-script
1.144 - '())
1.145 + '("inductive_cases"))
1.146
1.147 (defconst isar-keywords-theory-goal
1.148 '("corollary"
2.1 --- a/etc/isar-keywords.el Mon May 11 09:18:42 2009 +0200
2.2 +++ b/etc/isar-keywords.el Mon May 11 09:39:53 2009 +0200
2.3 @@ -1,6 +1,6 @@
2.4 ;;
2.5 ;; Keyword classification tables for Isabelle/Isar.
2.6 -;; Generated from Pure + Pure-ProofGeneral + HOL + HOLCF + IOA + HOL-Nominal + HOL-Statespace + HOL-ex.
2.7 +;; Generated from Pure + Pure-ProofGeneral + HOL + HOLCF + IOA + HOL-Nominal + HOL-Statespace.
2.8 ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
2.9 ;;
2.10
2.11 @@ -36,6 +36,7 @@
2.12 "atp_kill"
2.13 "atp_messages"
2.14 "attribute_setup"
2.15 + "automaton"
2.16 "ax_specification"
2.17 "axclass"
2.18 "axiomatization"
2.19 @@ -73,6 +74,7 @@
2.20 "consts_code"
2.21 "context"
2.22 "corollary"
2.23 + "cpodef"
2.24 "datatype"
2.25 "declaration"
2.26 "declare"
2.27 @@ -84,6 +86,7 @@
2.28 "defs"
2.29 "disable_pr"
2.30 "display_drafts"
2.31 + "domain"
2.32 "done"
2.33 "enable_pr"
2.34 "end"
2.35 @@ -97,6 +100,8 @@
2.36 "find_consts"
2.37 "find_theorems"
2.38 "fix"
2.39 + "fixpat"
2.40 + "fixrec"
2.41 "from"
2.42 "full_prf"
2.43 "fun"
2.44 @@ -146,6 +151,7 @@
2.45 "overloading"
2.46 "parse_ast_translation"
2.47 "parse_translation"
2.48 + "pcpodef"
2.49 "pr"
2.50 "prefer"
2.51 "presume"
2.52 @@ -249,13 +255,15 @@
2.53 "}"))
2.54
2.55 (defconst isar-keywords-minor
2.56 - '("advanced"
2.57 + '("actions"
2.58 + "advanced"
2.59 "and"
2.60 "assumes"
2.61 "attach"
2.62 "avoids"
2.63 "begin"
2.64 "binder"
2.65 + "compose"
2.66 "congs"
2.67 "constrains"
2.68 "contains"
2.69 @@ -263,6 +271,7 @@
2.70 "file"
2.71 "fixes"
2.72 "for"
2.73 + "hide_action"
2.74 "hints"
2.75 "identifier"
2.76 "if"
2.77 @@ -271,7 +280,11 @@
2.78 "infix"
2.79 "infixl"
2.80 "infixr"
2.81 + "initially"
2.82 + "inputs"
2.83 + "internals"
2.84 "is"
2.85 + "lazy"
2.86 "module_name"
2.87 "monos"
2.88 "morphisms"
2.89 @@ -279,10 +292,20 @@
2.90 "obtains"
2.91 "open"
2.92 "output"
2.93 + "outputs"
2.94 "overloaded"
2.95 "permissive"
2.96 + "post"
2.97 + "pre"
2.98 + "rename"
2.99 + "restrict"
2.100 "shows"
2.101 + "signature"
2.102 + "states"
2.103 "structure"
2.104 + "to"
2.105 + "transitions"
2.106 + "transrel"
2.107 "unchecked"
2.108 "uses"
2.109 "where"))
2.110 @@ -400,6 +423,7 @@
2.111 "arities"
2.112 "atom_decl"
2.113 "attribute_setup"
2.114 + "automaton"
2.115 "axclass"
2.116 "axiomatization"
2.117 "axioms"
2.118 @@ -431,10 +455,13 @@
2.119 "defer_recdef"
2.120 "definition"
2.121 "defs"
2.122 + "domain"
2.123 "equivariance"
2.124 "extract"
2.125 "extract_type"
2.126 "finalconsts"
2.127 + "fixpat"
2.128 + "fixrec"
2.129 "fun"
2.130 "global"
2.131 "hide"
2.132 @@ -487,6 +514,7 @@
2.133 '("ax_specification"
2.134 "code_pred"
2.135 "corollary"
2.136 + "cpodef"
2.137 "function"
2.138 "instance"
2.139 "interpretation"
2.140 @@ -494,6 +522,7 @@
2.141 "nominal_inductive"
2.142 "nominal_inductive2"
2.143 "nominal_primrec"
2.144 + "pcpodef"
2.145 "recdef_tc"
2.146 "rep_datatype"
2.147 "specification"
3.1 --- a/lib/jedit/isabelle.xml Mon May 11 09:18:42 2009 +0200
3.2 +++ b/lib/jedit/isabelle.xml Mon May 11 09:39:53 2009 +0200
3.3 @@ -47,6 +47,7 @@
3.4 <OPERATOR>ML_prf</OPERATOR>
3.5 <LABEL>ML_val</LABEL>
3.6 <OPERATOR>abbreviation</OPERATOR>
3.7 + <KEYWORD4>actions</KEYWORD4>
3.8 <KEYWORD4>advanced</KEYWORD4>
3.9 <OPERATOR>also</OPERATOR>
3.10 <KEYWORD4>and</KEYWORD4>
3.11 @@ -61,6 +62,7 @@
3.12 <LABEL>atp_messages</LABEL>
3.13 <KEYWORD4>attach</KEYWORD4>
3.14 <OPERATOR>attribute_setup</OPERATOR>
3.15 + <OPERATOR>automaton</OPERATOR>
3.16 <KEYWORD4>avoids</KEYWORD4>
3.17 <OPERATOR>ax_specification</OPERATOR>
3.18 <OPERATOR>axclass</OPERATOR>
3.19 @@ -72,12 +74,14 @@
3.20 <OPERATOR>by</OPERATOR>
3.21 <INVALID>cannot_undo</INVALID>
3.22 <KEYWORD2>case</KEYWORD2>
3.23 + <KEYWORD4>case_eqns</KEYWORD4>
3.24 <LABEL>cd</LABEL>
3.25 <OPERATOR>chapter</OPERATOR>
3.26 <OPERATOR>class</OPERATOR>
3.27 <LABEL>class_deps</LABEL>
3.28 <OPERATOR>classes</OPERATOR>
3.29 <OPERATOR>classrel</OPERATOR>
3.30 + <OPERATOR>codatatype</OPERATOR>
3.31 <OPERATOR>code_abort</OPERATOR>
3.32 <OPERATOR>code_class</OPERATOR>
3.33 <OPERATOR>code_const</OPERATOR>
3.34 @@ -89,12 +93,15 @@
3.35 <OPERATOR>code_module</OPERATOR>
3.36 <OPERATOR>code_modulename</OPERATOR>
3.37 <OPERATOR>code_monad</OPERATOR>
3.38 + <OPERATOR>code_pred</OPERATOR>
3.39 <OPERATOR>code_reserved</OPERATOR>
3.40 <LABEL>code_thms</LABEL>
3.41 <OPERATOR>code_type</OPERATOR>
3.42 <OPERATOR>coinductive</OPERATOR>
3.43 <OPERATOR>coinductive_set</OPERATOR>
3.44 <LABEL>commit</LABEL>
3.45 + <KEYWORD4>compose</KEYWORD4>
3.46 + <KEYWORD4>con_defs</KEYWORD4>
3.47 <KEYWORD4>congs</KEYWORD4>
3.48 <OPERATOR>constdefs</OPERATOR>
3.49 <KEYWORD4>constrains</KEYWORD4>
3.50 @@ -103,6 +110,7 @@
3.51 <KEYWORD4>contains</KEYWORD4>
3.52 <OPERATOR>context</OPERATOR>
3.53 <OPERATOR>corollary</OPERATOR>
3.54 + <OPERATOR>cpodef</OPERATOR>
3.55 <OPERATOR>datatype</OPERATOR>
3.56 <OPERATOR>declaration</OPERATOR>
3.57 <OPERATOR>declare</OPERATOR>
3.58 @@ -115,7 +123,10 @@
3.59 <OPERATOR>defs</OPERATOR>
3.60 <LABEL>disable_pr</LABEL>
3.61 <LABEL>display_drafts</LABEL>
3.62 + <OPERATOR>domain</OPERATOR>
3.63 + <KEYWORD4>domains</KEYWORD4>
3.64 <OPERATOR>done</OPERATOR>
3.65 + <KEYWORD4>elimination</KEYWORD4>
3.66 <LABEL>enable_pr</LABEL>
3.67 <KEYWORD3>end</KEYWORD3>
3.68 <OPERATOR>equivariance</OPERATOR>
3.69 @@ -130,6 +141,8 @@
3.70 <LABEL>find_theorems</LABEL>
3.71 <KEYWORD2>fix</KEYWORD2>
3.72 <KEYWORD4>fixes</KEYWORD4>
3.73 + <OPERATOR>fixpat</OPERATOR>
3.74 + <OPERATOR>fixrec</OPERATOR>
3.75 <KEYWORD4>for</KEYWORD4>
3.76 <OPERATOR>from</OPERATOR>
3.77 <LABEL>full_prf</LABEL>
3.78 @@ -142,11 +155,13 @@
3.79 <LABEL>help</LABEL>
3.80 <OPERATOR>hence</OPERATOR>
3.81 <OPERATOR>hide</OPERATOR>
3.82 + <KEYWORD4>hide_action</KEYWORD4>
3.83 <KEYWORD4>hints</KEYWORD4>
3.84 <KEYWORD4>identifier</KEYWORD4>
3.85 <KEYWORD4>if</KEYWORD4>
3.86 <KEYWORD4>imports</KEYWORD4>
3.87 <KEYWORD4>in</KEYWORD4>
3.88 + <KEYWORD4>induction</KEYWORD4>
3.89 <OPERATOR>inductive</OPERATOR>
3.90 <KEYWORD1>inductive_cases</KEYWORD1>
3.91 <OPERATOR>inductive_set</OPERATOR>
3.92 @@ -154,14 +169,19 @@
3.93 <KEYWORD4>infixl</KEYWORD4>
3.94 <KEYWORD4>infixr</KEYWORD4>
3.95 <INVALID>init_toplevel</INVALID>
3.96 + <KEYWORD4>initially</KEYWORD4>
3.97 + <KEYWORD4>inputs</KEYWORD4>
3.98 <OPERATOR>instance</OPERATOR>
3.99 <OPERATOR>instantiation</OPERATOR>
3.100 + <KEYWORD4>internals</KEYWORD4>
3.101 <OPERATOR>interpret</OPERATOR>
3.102 <OPERATOR>interpretation</OPERATOR>
3.103 + <KEYWORD4>intros</KEYWORD4>
3.104 <KEYWORD4>is</KEYWORD4>
3.105 <OPERATOR>judgment</OPERATOR>
3.106 <INVALID>kill</INVALID>
3.107 <LABEL>kill_thy</LABEL>
3.108 + <KEYWORD4>lazy</KEYWORD4>
3.109 <OPERATOR>lemma</OPERATOR>
3.110 <OPERATOR>lemmas</OPERATOR>
3.111 <OPERATOR>let</OPERATOR>
3.112 @@ -193,12 +213,16 @@
3.113 <KEYWORD4>open</KEYWORD4>
3.114 <OPERATOR>oracle</OPERATOR>
3.115 <KEYWORD4>output</KEYWORD4>
3.116 + <KEYWORD4>outputs</KEYWORD4>
3.117 <KEYWORD4>overloaded</KEYWORD4>
3.118 <OPERATOR>overloading</OPERATOR>
3.119 <OPERATOR>parse_ast_translation</OPERATOR>
3.120 <OPERATOR>parse_translation</OPERATOR>
3.121 + <OPERATOR>pcpodef</OPERATOR>
3.122 <KEYWORD4>permissive</KEYWORD4>
3.123 + <KEYWORD4>post</KEYWORD4>
3.124 <LABEL>pr</LABEL>
3.125 + <KEYWORD4>pre</KEYWORD4>
3.126 <KEYWORD1>prefer</KEYWORD1>
3.127 <KEYWORD2>presume</KEYWORD2>
3.128 <LABEL>pretty_setmargin</LABEL>
3.129 @@ -228,6 +252,7 @@
3.130 <LABEL>print_simpset</LABEL>
3.131 <LABEL>print_statement</LABEL>
3.132 <LABEL>print_syntax</LABEL>
3.133 + <LABEL>print_tcset</LABEL>
3.134 <LABEL>print_theorems</LABEL>
3.135 <LABEL>print_theory</LABEL>
3.136 <LABEL>print_trans_rules</LABEL>
3.137 @@ -244,19 +269,24 @@
3.138 <OPERATOR>recdef</OPERATOR>
3.139 <OPERATOR>recdef_tc</OPERATOR>
3.140 <OPERATOR>record</OPERATOR>
3.141 + <KEYWORD4>recursor_eqns</KEYWORD4>
3.142 <LABEL>refute</LABEL>
3.143 <OPERATOR>refute_params</OPERATOR>
3.144 <LABEL>remove_thy</LABEL>
3.145 + <KEYWORD4>rename</KEYWORD4>
3.146 <OPERATOR>rep_datatype</OPERATOR>
3.147 + <KEYWORD4>restrict</KEYWORD4>
3.148 <OPERATOR>sect</OPERATOR>
3.149 <OPERATOR>section</OPERATOR>
3.150 <OPERATOR>setup</OPERATOR>
3.151 <KEYWORD2>show</KEYWORD2>
3.152 <KEYWORD4>shows</KEYWORD4>
3.153 + <KEYWORD4>signature</KEYWORD4>
3.154 <OPERATOR>simproc_setup</OPERATOR>
3.155 <LABEL>sledgehammer</LABEL>
3.156 <OPERATOR>sorry</OPERATOR>
3.157 <OPERATOR>specification</OPERATOR>
3.158 + <KEYWORD4>states</KEYWORD4>
3.159 <OPERATOR>statespace</OPERATOR>
3.160 <KEYWORD4>structure</KEYWORD4>
3.161 <OPERATOR>subclass</OPERATOR>
3.162 @@ -278,11 +308,16 @@
3.163 <LABEL>thm_deps</LABEL>
3.164 <KEYWORD2>thus</KEYWORD2>
3.165 <LABEL>thy_deps</LABEL>
3.166 + <KEYWORD4>to</KEYWORD4>
3.167 <LABEL>touch_thy</LABEL>
3.168 + <KEYWORD4>transitions</KEYWORD4>
3.169 <OPERATOR>translations</OPERATOR>
3.170 + <KEYWORD4>transrel</KEYWORD4>
3.171 <OPERATOR>txt</OPERATOR>
3.172 <OPERATOR>txt_raw</OPERATOR>
3.173 <LABEL>typ</LABEL>
3.174 + <KEYWORD4>type_elims</KEYWORD4>
3.175 + <KEYWORD4>type_intros</KEYWORD4>
3.176 <OPERATOR>typed_print_translation</OPERATOR>
3.177 <OPERATOR>typedecl</OPERATOR>
3.178 <OPERATOR>typedef</OPERATOR>
4.1 --- a/src/HOL/ex/Predicate_Compile.thy Mon May 11 09:18:42 2009 +0200
4.2 +++ b/src/HOL/ex/Predicate_Compile.thy Mon May 11 09:39:53 2009 +0200
4.3 @@ -49,6 +49,7 @@
4.4 code_pred append
4.5 using assms by (rule append.cases)
4.6
4.7 +thm append_codegen
4.8 thm append_cases
4.9
4.10
5.1 --- a/src/HOL/ex/predicate_compile.ML Mon May 11 09:18:42 2009 +0200
5.2 +++ b/src/HOL/ex/predicate_compile.ML Mon May 11 09:39:53 2009 +0200
5.3 @@ -1378,18 +1378,18 @@
5.4 val const = prep_const thy raw_const
5.5 val nparams = get_nparams thy const
5.6 val intro_rules = pred_intros thy const
5.7 - val (((tfrees, frees), fact), ctxt') =
5.8 + val (((tfrees, frees), fact), lthy') =
5.9 Variable.import_thms true intro_rules lthy;
5.10 - val (pred, prop, ctxt'') = mk_casesrule fact nparams ctxt'
5.11 + val (pred, prop, lthy'') = mk_casesrule fact nparams lthy'
5.12 val (predname, _) = dest_Const pred
5.13 - fun after_qed [[th]] ctxt'' =
5.14 + fun after_qed [[th]] lthy'' =
5.15 LocalTheory.note Thm.theoremK
5.16 - ((Binding.name (Long_Name.base_name predname ^ "_cases"),
5.17 - [Attrib.internal (K (code_ind_cases_attrib))]) , [th]) ctxt''
5.18 + ((Binding.name (Long_Name.base_name predname ^ "_cases"), (* FIXME: other suffix *)
5.19 + [Attrib.internal (K (code_ind_cases_attrib))]) , [th]) lthy''
5.20 |> snd
5.21 - |> ProofContext.theory (create_def_equation predname)
5.22 + |> LocalTheory.theory (create_def_equation predname)
5.23 in
5.24 - Proof.theorem_i NONE after_qed [[(prop, [])]] ctxt''
5.25 + Proof.theorem_i NONE after_qed [[(prop, [])]] lthy''
5.26 end;
5.27
5.28 val code_pred = generic_code_pred (K I);