# HG changeset patch # User blanchet # Date 1410454476 -7200 # Node ID 57752a91eec44712ec639c4d0906528de6af9c08 # Parent acc2f1801acc9a4ae875292029a8bfb937ca5976 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new' diff -r acc2f1801acc -r 57752a91eec4 src/Doc/Codegen/Evaluation.thy --- a/src/Doc/Codegen/Evaluation.thy Thu Sep 11 18:54:36 2014 +0200 +++ b/src/Doc/Codegen/Evaluation.thy Thu Sep 11 18:54:36 2014 +0200 @@ -205,7 +205,7 @@ An simplistic example: *} -datatype %quote form_ord = T | F | Less nat nat +datatype_new %quote form_ord = T | F | Less nat nat | And form_ord form_ord | Or form_ord form_ord | Neg form_ord primrec %quote interp :: "form_ord \ 'a::order list \ bool" @@ -259,7 +259,7 @@ example: *} -datatype %quote form = T | F | And form form | Or form form (*<*) +datatype_new %quote form = T | F | And form form | Or form form (*<*) (*>*) ML %quotett {* fun eval_form @{code T} = true diff -r acc2f1801acc -r 57752a91eec4 src/Doc/Codegen/Introduction.thy --- a/src/Doc/Codegen/Introduction.thy Thu Sep 11 18:54:36 2014 +0200 +++ b/src/Doc/Codegen/Introduction.thy Thu Sep 11 18:54:36 2014 +0200 @@ -35,7 +35,7 @@ subsection {* A quick start with the Isabelle/HOL toolbox \label{sec:queue_example} *} text {* - In a HOL theory, the @{command_def datatype} and @{command_def + In a HOL theory, the @{command_def datatype_new} and @{command_def definition}/@{command_def primrec}/@{command_def fun} declarations form the core of a functional programming language. By default equational theorems stemming from those are used for generated code, @@ -45,7 +45,7 @@ For example, here a simple \qt{implementation} of amortised queues: *} -datatype %quote 'a queue = AQueue "'a list" "'a list" +datatype_new %quote 'a queue = AQueue "'a list" "'a list" definition %quote empty :: "'a queue" where "empty = AQueue [] []" diff -r acc2f1801acc -r 57752a91eec4 src/Doc/Codegen/Refinement.thy --- a/src/Doc/Codegen/Refinement.thy Thu Sep 11 18:54:36 2014 +0200 +++ b/src/Doc/Codegen/Refinement.thy Thu Sep 11 18:54:36 2014 +0200 @@ -87,7 +87,7 @@ queues: *} -datatype %quote 'a queue = Queue "'a list" +datatype_new %quote 'a queue = Queue "'a list" definition %quote empty :: "'a queue" where "empty = Queue []" diff -r acc2f1801acc -r 57752a91eec4 src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Thu Sep 11 18:54:36 2014 +0200 +++ b/src/Doc/Datatypes/Datatypes.thy Thu Sep 11 18:54:36 2014 +0200 @@ -5,7 +5,7 @@ Author: Andrei Popescu, TU Muenchen Author: Dmitriy Traytel, TU Muenchen -Tutorial for (co)datatype definitions with the new package. +Tutorial for (co)datatype definitions. *) theory Datatypes @@ -21,14 +21,9 @@ \label{sec:introduction} *} text {* -The 2013 edition of Isabelle introduced a new definitional package for freely -generated datatypes and codatatypes. The datatype support is similar to that -provided by the earlier package due to Berghofer and Wenzel -\cite{Berghofer-Wenzel:1999:TPHOL}, documented in the Isar reference manual -\cite{isabelle-isar-ref}; indeed, replacing the keyword \keyw{datatype} by -@{command datatype_new} is often all that is needed to port existing theories to -use the new package. - +The 2013 edition of Isabelle introduced a definitional package for freely +generated datatypes and codatatypes. This package replaces the earlier +implementation due to Berghofer and Wenzel \cite{Berghofer-Wenzel:1999:TPHOL}. Perhaps the main advantage of the new package is that it supports recursion through a large class of non-datatypes, such as finite sets: *} @@ -51,7 +46,7 @@ generated discriminators, selectors, and relators as well as a wealth of properties about them. -In addition to inductive datatypes, the new package supports coinductive +In addition to inductive datatypes, the package supports coinductive datatypes, or \emph{codatatypes}, which allow infinite values. For example, the following command introduces the type of lazy lists, which comprises both finite and infinite values: @@ -151,12 +146,8 @@ \newcommand\authoremailv{\texttt{tray{\color{white}NOSPAM}\kern-\wd\boxA{}tel@\allowbreak in.\allowbreak tum.\allowbreak de}} -The command @{command datatype_new} is expected to replace \keyw{datatype} in a -future release. Authors of new theories are encouraged to use the new commands, -and maintainers of older theories may want to consider upgrading. - -Comments and bug reports concerning either the tool or this tutorial should be -directed to the authors at \authoremaili, \authoremailii, \authoremailiii, +Comments and bug reports concerning either the package or this tutorial should +be directed to the authors at \authoremaili, \authoremailii, \authoremailiii, \authoremailiv, and \authoremailv. *} @@ -1036,8 +1027,9 @@ text {* The command @{command datatype_new} has been designed to be highly compatible -with the old \keyw{datatype}, to ease migration. There are nonetheless a few -incompatibilities that may arise when porting to the new package: +with the old command (which is now called \keyw{old_datatype}), to ease +migration. There are nonetheless a few incompatibilities that may arise when +porting: \begin{itemize} \setlength{\itemsep}{0pt} @@ -1065,8 +1057,8 @@ @{text "[unfolded all_mem_range]"} attribute on @{text t.induct}. \item \emph{The internal constructions are completely different.} Proof texts -that unfold the definition of constants introduced by \keyw{datatype} will be -difficult to port. +that unfold the definition of constants introduced by \keyw{old\_datatype} will +be difficult to port. \item \emph{Some constants and theorems have different names.} For non-mutually recursive datatypes, @@ -2696,9 +2688,6 @@ % * need for this is rare but may arise if you want e.g. to add destructors to % a type not introduced by ... % -% * also useful for compatibility with old package, e.g. add destructors to -% old \keyw{datatype} -% % * @{command free_constructors} % * @{text plugins}, @{text discs_sels} % * hack to have both co and nonco view via locale (cf. ext nats) diff -r acc2f1801acc -r 57752a91eec4 src/Doc/Datatypes/document/root.tex --- a/src/Doc/Datatypes/document/root.tex Thu Sep 11 18:54:36 2014 +0200 +++ b/src/Doc/Datatypes/document/root.tex Thu Sep 11 18:54:36 2014 +0200 @@ -76,10 +76,9 @@ \begin{abstract} \noindent -This tutorial describes the new package for defining datatypes and codatatypes +This tutorial describes the definitional package for datatypes and codatatypes in Isabelle/HOL. The package provides four main commands: \keyw{datatype_new}, -\keyw{codatatype}, \keyw{primrec}, and \keyw{primcorec}. The first command is -expected to eventually replace the old \keyw{datatype} command. +\keyw{codatatype}, \keyw{primrec}, and \keyw{primcorec}. \end{abstract} \tableofcontents diff -r acc2f1801acc -r 57752a91eec4 src/Doc/Functions/Functions.thy --- a/src/Doc/Functions/Functions.thy Thu Sep 11 18:54:36 2014 +0200 +++ b/src/Doc/Functions/Functions.thy Thu Sep 11 18:54:36 2014 +0200 @@ -522,7 +522,7 @@ and @{term "X"} for true, false and uncertain propositions, respectively. *} -datatype P3 = T | F | X +datatype_new P3 = T | F | X text {* \noindent Then the conjunction of such values can be defined as follows: *} @@ -1122,7 +1122,7 @@ As an example, imagine a datatype of n-ary trees: *} -datatype 'a tree = +datatype_new 'a tree = Leaf 'a | Branch "'a tree list" diff -r acc2f1801acc -r 57752a91eec4 src/Doc/Isar_Ref/Generic.thy --- a/src/Doc/Isar_Ref/Generic.thy Thu Sep 11 18:54:36 2014 +0200 +++ b/src/Doc/Isar_Ref/Generic.thy Thu Sep 11 18:54:36 2014 +0200 @@ -736,7 +736,7 @@ monotonically through the theory hierarchy: forming a new theory, the union of the simpsets of its imports are taken as starting point. Also note that definitional packages like @{command - "datatype"}, @{command "primrec"}, @{command "fun"} routinely + "datatype_new"}, @{command "primrec"}, @{command "fun"} routinely declare Simplifier rules to the target context, while plain @{command "definition"} is an exception in \emph{not} declaring anything. diff -r acc2f1801acc -r 57752a91eec4 src/Doc/Isar_Ref/HOL_Specific.thy --- a/src/Doc/Isar_Ref/HOL_Specific.thy Thu Sep 11 18:54:36 2014 +0200 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy Thu Sep 11 18:54:36 2014 +0200 @@ -283,11 +283,10 @@ \begin{description} \item @{command (HOL) "primrec"} defines primitive recursive - functions over datatypes (see also @{command_ref (HOL) datatype} and - @{command_ref (HOL) rep_datatype}). The given @{text equations} - specify reduction rules that are produced by instantiating the - generic combinator for primitive recursion that is available for - each datatype. + functions over datatypes (see also @{command_ref (HOL) datatype_new}). + The given @{text equations} specify reduction rules that are produced + by instantiating the generic combinator for primitive recursion that + is available for each datatype. Each equation needs to be of the form: @@ -379,7 +378,7 @@ boolean expressions, and use @{command primrec} for evaluation functions that follow the same recursive structure. *} -datatype 'a aexp = +datatype_new 'a aexp = IF "'a bexp" "'a aexp" "'a aexp" | Sum "'a aexp" "'a aexp" | Diff "'a aexp" "'a aexp" @@ -450,7 +449,7 @@ text {* Functions on datatypes with nested recursion are also defined by mutual primitive recursion. *} -datatype ('a, 'b) "term" = Var 'a | App 'b "('a, 'b) term list" +datatype_new ('a, 'b) "term" = Var 'a | App 'b "('a, 'b) term list" text {* A substitution function on type @{typ "('a, 'b) term"} can be defined as follows, by working simultaneously on @{typ "('a, 'b) @@ -471,7 +470,7 @@ lemma "subst_term (subst_term f1 \ f2) t = subst_term f1 (subst_term f2 t)" and "subst_term_list (subst_term f1 \ f2) ts = subst_term_list f1 (subst_term_list f2 ts)" - by (induct t and ts) simp_all + by (induct t and ts rule: subst_term.induct subst_term_list.induct) simp_all subsubsection {* Example: a map function for infinitely branching trees *} @@ -480,7 +479,7 @@ primitive recursion is just as easy. *} -datatype 'a tree = Atom 'a | Branch "nat \ 'a tree" +datatype_new 'a tree = Atom 'a | Branch "nat \ 'a tree" primrec map_tree :: "('a \ 'b) \ 'a tree \ 'b tree" where @@ -702,16 +701,16 @@ *} -section {* Datatypes \label{sec:hol-datatype} *} +section {* Old-style datatypes \label{sec:hol-datatype} *} text {* \begin{matharray}{rcl} - @{command_def (HOL) "datatype"} & : & @{text "theory \ theory"} \\ + @{command_def (HOL) "old_datatype"} & : & @{text "theory \ theory"} \\ @{command_def (HOL) "rep_datatype"} & : & @{text "theory \ proof(prove)"} \\ \end{matharray} @{rail \ - @@{command (HOL) datatype} (spec + @'and') + @@{command (HOL) old_datatype} (spec + @'and') ; @@{command (HOL) rep_datatype} ('(' (@{syntax name} +) ')')? (@{syntax term} +) ; @@ -723,30 +722,16 @@ \begin{description} - \item @{command (HOL) "datatype"} defines inductive datatypes in - HOL. + \item @{command (HOL) "old_datatype"} defines old-style inductive + datatypes in HOL. \item @{command (HOL) "rep_datatype"} represents existing types as - datatypes. - - For foundational reasons, some basic types such as @{typ nat}, @{typ - "'a \ 'b"}, @{typ "'a + 'b"}, @{typ bool} and @{typ unit} are - introduced by more primitive means using @{command_ref typedef}. To - recover the rich infrastructure of @{command datatype} (e.g.\ rules - for @{method cases} and @{method induct} and the primitive recursion - combinators), such types may be represented as actual datatypes - later. This is done by specifying the constructors of the desired - type, and giving a proof of the induction rule, distinctness and - injectivity of constructors. - - For example, see @{file "~~/src/HOL/Sum_Type.thy"} for the - representation of the primitive sum type as fully-featured datatype. + old-style datatypes. \end{description} - The generated rules for @{method induct} and @{method cases} provide - case names according to the given constructors, while parameters are - named after the types (see also \secref{sec:cases-induct}). + These commands are mostly obsolete; @{command (HOL) "datatype"} + should be used instead. See \cite{isabelle-HOL} for more details on datatypes, but beware of the old-style theory syntax being used there! Apart from proper @@ -764,7 +749,7 @@ names than the existing @{typ "'a list"} that is already in @{theory Main}: *} -datatype 'a seq = Empty | Seq 'a "'a seq" +datatype_new 'a seq = Empty | Seq 'a "'a seq" text {* We can now prove some simple lemma by structural induction: *} @@ -1173,9 +1158,9 @@ by (cases x) (auto simp: One_def Two_def Three_def Abs_three_inject) text {* Note that such trivial constructions are better done with - derived specification mechanisms such as @{command datatype}: *} - -datatype three' = One' | Two' | Three' + derived specification mechanisms such as @{command datatype_new}: *} + +datatype_new three' = One' | Two' | Three' text {* This avoids re-doing basic definitions and proofs from the primitive @{command typedef} above. *} @@ -2369,7 +2354,7 @@ to reason about inductive types. Rules are selected according to the declarations by the @{attribute cases} and @{attribute induct} attributes, cf.\ \secref{sec:cases-induct}. The @{command (HOL) - datatype} package already takes care of this. + datatype_new} package already takes care of this. These unstructured tactics feature both goal addressing and dynamic instantiation. Note that named rule cases are \emph{not} provided diff -r acc2f1801acc -r 57752a91eec4 src/Doc/Isar_Ref/Spec.thy --- a/src/Doc/Isar_Ref/Spec.thy Thu Sep 11 18:54:36 2014 +0200 +++ b/src/Doc/Isar_Ref/Spec.thy Thu Sep 11 18:54:36 2014 +0200 @@ -81,7 +81,7 @@ the formal text. Examples may be seen in Isabelle/HOL sources itself, such as @{keyword "keywords"}~@{verbatim "\"typedef\""} @{text ":: thy_goal"} or @{keyword "keywords"}~@{verbatim - "\"datatype\""} @{text ":: thy_decl"} for theory-level declarations + "\"old_datatype\""} @{text ":: thy_decl"} for theory-level declarations with and without proof, respectively. Additional @{syntax tags} provide defaults for document preparation (\secref{sec:tags}). diff -r acc2f1801acc -r 57752a91eec4 src/Doc/Isar_Ref/Synopsis.thy --- a/src/Doc/Isar_Ref/Synopsis.thy Thu Sep 11 18:54:36 2014 +0200 +++ b/src/Doc/Isar_Ref/Synopsis.thy Thu Sep 11 18:54:36 2014 +0200 @@ -1068,7 +1068,7 @@ provide suitable derived cases rules. *} -datatype foo = Foo | Bar foo +datatype_new foo = Foo | Bar foo notepad begin diff -r acc2f1801acc -r 57752a91eec4 src/Doc/Tutorial/CodeGen/CodeGen.thy --- a/src/Doc/Tutorial/CodeGen/CodeGen.thy Thu Sep 11 18:54:36 2014 +0200 +++ b/src/Doc/Tutorial/CodeGen/CodeGen.thy Thu Sep 11 18:54:36 2014 +0200 @@ -16,9 +16,9 @@ *} type_synonym 'v binop = "'v \ 'v \ 'v"; -datatype ('a,'v)expr = Cex 'v - | Vex 'a - | Bex "'v binop" "('a,'v)expr" "('a,'v)expr"; +datatype (dead 'a, 'v) expr = Cex 'v + | Vex 'a + | Bex "'v binop" "('a,'v)expr" "('a,'v)expr"; text{*\noindent The three constructors represent constants, variables and the application of @@ -40,7 +40,7 @@ the result. As for @{text"expr"}, addresses and values are type parameters: *} -datatype ('a,'v) instr = Const 'v +datatype (dead 'a, 'v) instr = Const 'v | Load 'a | Apply "'v binop"; diff -r acc2f1801acc -r 57752a91eec4 src/Doc/Tutorial/Datatype/Fundata.thy --- a/src/Doc/Tutorial/Datatype/Fundata.thy Thu Sep 11 18:54:36 2014 +0200 +++ b/src/Doc/Tutorial/Datatype/Fundata.thy Thu Sep 11 18:54:36 2014 +0200 @@ -1,7 +1,7 @@ (*<*) theory Fundata imports Main begin (*>*) -datatype ('a,'i)bigtree = Tip | Br 'a "'i \ ('a,'i)bigtree" +datatype (dead 'a,'i) bigtree = Tip | Br 'a "'i \ ('a,'i)bigtree" text{*\noindent Parameter @{typ"'a"} is the type of values stored in diff -r acc2f1801acc -r 57752a91eec4 src/Doc/Tutorial/Datatype/Nested.thy --- a/src/Doc/Tutorial/Datatype/Nested.thy Thu Sep 11 18:54:36 2014 +0200 +++ b/src/Doc/Tutorial/Datatype/Nested.thy Thu Sep 11 18:54:36 2014 +0200 @@ -67,7 +67,7 @@ lemma subst_id(*<*)(*referred to from ABexpr*)(*>*): "subst Var t = (t ::('v,'f)term) \ substs Var ts = (ts::('v,'f)term list)"; -apply(induct_tac t and ts, simp_all); +apply(induct_tac t and ts rule: subst.induct substs.induct, simp_all); done text{*\noindent @@ -105,7 +105,7 @@ (* Exercise 1: *) lemma "subst ((subst f) \ g) t = subst f (subst g t) \ substs ((subst f) \ g) ts = substs f (substs g ts)" -apply (induct_tac t and ts) +apply (induct_tac t and ts rule: subst.induct substs.induct) apply (simp_all) done @@ -125,7 +125,7 @@ lemma "trev (trev t) = (t::('v,'f)term) \ trevs (trevs ts) = (ts::('v,'f)term list)" -apply (induct_tac t and ts, simp_all) +apply (induct_tac t and ts rule: trev.induct trevs.induct, simp_all) done (*>*) diff -r acc2f1801acc -r 57752a91eec4 src/Doc/Tutorial/Protocol/Message.thy --- a/src/Doc/Tutorial/Protocol/Message.thy Thu Sep 11 18:54:36 2014 +0200 +++ b/src/Doc/Tutorial/Protocol/Message.thy Thu Sep 11 18:54:36 2014 +0200 @@ -334,6 +334,7 @@ txt{*MPair case: blast works out the necessary sum itself!*} prefer 2 apply auto apply (blast elim!: add_leE) txt{*Nonce case*} +apply (rename_tac nat) apply (rule_tac x = "N + Suc nat" in exI, auto) done (*>*) diff -r acc2f1801acc -r 57752a91eec4 src/Doc/Tutorial/Trie/Trie.thy --- a/src/Doc/Tutorial/Trie/Trie.thy Thu Sep 11 18:54:36 2014 +0200 +++ b/src/Doc/Tutorial/Trie/Trie.thy Thu Sep 11 18:54:36 2014 +0200 @@ -208,7 +208,7 @@ (* Exercise 3. Solution by Getrud Bauer *) -datatype ('a,'v) triem = Triem "'v option" "'a \ ('a,'v) triem option"; +datatype ('a,dead 'v) triem = Triem "'v option" "'a \ ('a,'v) triem option"; primrec valuem :: "('a, 'v) triem \ 'v option" where "valuem (Triem ov m) = ov" diff -r acc2f1801acc -r 57752a91eec4 src/HOL/Auth/Event.thy --- a/src/HOL/Auth/Event.thy Thu Sep 11 18:54:36 2014 +0200 +++ b/src/HOL/Auth/Event.thy Thu Sep 11 18:54:36 2014 +0200 @@ -15,7 +15,7 @@ consts (*Initial states of agents -- parameter of the construction*) initState :: "agent => msg set" -datatype +datatype_new event = Says agent agent msg | Gets agent msg | Notes agent msg diff -r acc2f1801acc -r 57752a91eec4 src/HOL/Auth/Guard/Extensions.thy --- a/src/HOL/Auth/Guard/Extensions.thy Thu Sep 11 18:54:36 2014 +0200 +++ b/src/HOL/Auth/Guard/Extensions.thy Thu Sep 11 18:54:36 2014 +0200 @@ -579,6 +579,7 @@ apply (drule_tac P="%G. X:parts G" in knows_Cons_substD, safe) apply (erule initState_used) apply (case_tac a, auto) +apply (rename_tac msg) apply (drule_tac B=A and X=msg and evs=evs in Gets_correct_Says) by (auto dest: Says_imp_used intro: used_ConsI) @@ -592,6 +593,7 @@ apply (frule_tac ev=a and evs=evs in one_step_Cons, simp, clarify) apply (drule_tac P="%G. X:parts G" in knows_max_Cons_substD, safe) apply (case_tac a, auto) +apply (rename_tac msg) apply (drule_tac B=A and X=msg and evs=evs in Gets_correct_Says) by (auto simp: knows_max'_Cons dest: Says_imp_used intro: used_ConsI) diff -r acc2f1801acc -r 57752a91eec4 src/HOL/BNF_Examples/Compat.thy --- a/src/HOL/BNF_Examples/Compat.thy Thu Sep 11 18:54:36 2014 +0200 +++ b/src/HOL/BNF_Examples/Compat.thy Thu Sep 11 18:54:36 2014 +0200 @@ -27,7 +27,7 @@ |> tap (check_lens lens); \ -datatype 'a old_lst = Old_Nl | Old_Cns 'a "'a old_lst" +old_datatype 'a old_lst = Old_Nl | Old_Cns 'a "'a old_lst" ML \ get_descrs @{theory} (1, 1, 1) @{type_name old_lst}; \ @@ -169,11 +169,11 @@ ML \ get_descrs @{theory} (2, 2, 2) @{type_name foo'}; \ ML \ get_descrs @{theory} (2, 2, 2) @{type_name bar'}; \ -datatype funky = Funky "funky tre" | Funky' +old_datatype funky = Funky "funky tre" | Funky' ML \ get_descrs @{theory} (3, 3, 3) @{type_name funky}; \ -datatype fnky = Fnky "nat tre" +old_datatype fnky = Fnky "nat tre" ML \ get_descrs @{theory} (1, 1, 1) @{type_name fnky}; \ diff -r acc2f1801acc -r 57752a91eec4 src/HOL/BNF_Least_Fixpoint.thy --- a/src/HOL/BNF_Least_Fixpoint.thy Thu Sep 11 18:54:36 2014 +0200 +++ b/src/HOL/BNF_Least_Fixpoint.thy Thu Sep 11 18:54:36 2014 +0200 @@ -12,6 +12,7 @@ theory BNF_Least_Fixpoint imports BNF_Fixpoint_Base keywords + "datatype" :: thy_decl and "datatype_new" :: thy_decl and "datatype_compat" :: thy_decl begin diff -r acc2f1801acc -r 57752a91eec4 src/HOL/Datatype_Benchmark/Brackin.thy --- a/src/HOL/Datatype_Benchmark/Brackin.thy Thu Sep 11 18:54:36 2014 +0200 +++ b/src/HOL/Datatype_Benchmark/Brackin.thy Thu Sep 11 18:54:36 2014 +0200 @@ -5,13 +5,13 @@ theory Brackin imports Main begin -datatype T = +old_datatype T = X1 | X2 | X3 | X4 | X5 | X6 | X7 | X8 | X9 | X10 | X11 | X12 | X13 | X14 | X15 | X16 | X17 | X18 | X19 | X20 | X21 | X22 | X23 | X24 | X25 | X26 | X27 | X28 | X29 | X30 | X31 | X32 | X33 | X34 -datatype ('a, 'b, 'c) TY1 = +old_datatype ('a, 'b, 'c) TY1 = NoF | Fk 'a "('a, 'b, 'c) TY2" and ('a, 'b, 'c) TY2 = diff -r acc2f1801acc -r 57752a91eec4 src/HOL/Datatype_Benchmark/Instructions.thy --- a/src/HOL/Datatype_Benchmark/Instructions.thy Thu Sep 11 18:54:36 2014 +0200 +++ b/src/HOL/Datatype_Benchmark/Instructions.thy Thu Sep 11 18:54:36 2014 +0200 @@ -5,158 +5,158 @@ theory Instructions imports Main begin -datatype Size = Byte | Word | Long +old_datatype Size = Byte | Word | Long -datatype DataRegister - = RegD0 - | RegD1 - | RegD2 - | RegD3 - | RegD4 - | RegD5 - | RegD6 - | RegD7 +old_datatype DataRegister = + RegD0 +| RegD1 +| RegD2 +| RegD3 +| RegD4 +| RegD5 +| RegD6 +| RegD7 -datatype AddressRegister - = RegA0 - | RegA1 - | RegA2 - | RegA3 - | RegA4 - | RegA5 - | RegA6 - | RegA7 +old_datatype AddressRegister = + RegA0 +| RegA1 +| RegA2 +| RegA3 +| RegA4 +| RegA5 +| RegA6 +| RegA7 -datatype DataOrAddressRegister - = data DataRegister - | address AddressRegister +old_datatype DataOrAddressRegister = + data DataRegister +| address AddressRegister -datatype Condition - = Hi - | Ls - | Cc - | Cs - | Ne - | Eq - | Vc - | Vs - | Pl - | Mi - | Ge - | Lt - | Gt - | Le +old_datatype Condition = + Hi +| Ls +| Cc +| Cs +| Ne +| Eq +| Vc +| Vs +| Pl +| Mi +| Ge +| Lt +| Gt +| Le -datatype AddressingMode - = immediate nat - | direct DataOrAddressRegister - | indirect AddressRegister - | postinc AddressRegister - | predec AddressRegister - | indirectdisp nat AddressRegister - | indirectindex nat AddressRegister DataOrAddressRegister Size - | absolute nat - | pcdisp nat - | pcindex nat DataOrAddressRegister Size +old_datatype AddressingMode = + immediate nat +| direct DataOrAddressRegister +| indirect AddressRegister +| postinc AddressRegister +| predec AddressRegister +| indirectdisp nat AddressRegister +| indirectindex nat AddressRegister DataOrAddressRegister Size +| absolute nat +| pcdisp nat +| pcindex nat DataOrAddressRegister Size -datatype M68kInstruction - = ABCD AddressingMode AddressingMode - | ADD Size AddressingMode AddressingMode - | ADDA Size AddressingMode AddressRegister - | ADDI Size nat AddressingMode - | ADDQ Size nat AddressingMode - | ADDX Size AddressingMode AddressingMode - | AND Size AddressingMode AddressingMode - | ANDI Size nat AddressingMode - | ANDItoCCR nat - | ANDItoSR nat - | ASL Size AddressingMode DataRegister - | ASLW AddressingMode - | ASR Size AddressingMode DataRegister - | ASRW AddressingMode - | Bcc Condition Size nat - | BTST Size AddressingMode AddressingMode - | BCHG Size AddressingMode AddressingMode - | BCLR Size AddressingMode AddressingMode - | BSET Size AddressingMode AddressingMode - | BRA Size nat - | BSR Size nat - | CHK AddressingMode DataRegister - | CLR Size AddressingMode - | CMP Size AddressingMode DataRegister - | CMPA Size AddressingMode AddressRegister - | CMPI Size nat AddressingMode - | CMPM Size AddressRegister AddressRegister - | DBT DataRegister nat - | DBF DataRegister nat - | DBcc Condition DataRegister nat - | DIVS AddressingMode DataRegister - | DIVU AddressingMode DataRegister - | EOR Size DataRegister AddressingMode - | EORI Size nat AddressingMode - | EORItoCCR nat - | EORItoSR nat - | EXG DataOrAddressRegister DataOrAddressRegister - | EXT Size DataRegister - | ILLEGAL - | JMP AddressingMode - | JSR AddressingMode - | LEA AddressingMode AddressRegister - | LINK AddressRegister nat - | LSL Size AddressingMode DataRegister - | LSLW AddressingMode - | LSR Size AddressingMode DataRegister - | LSRW AddressingMode - | MOVE Size AddressingMode AddressingMode - | MOVEtoCCR AddressingMode - | MOVEtoSR AddressingMode - | MOVEfromSR AddressingMode - | MOVEtoUSP AddressingMode - | MOVEfromUSP AddressingMode - | MOVEA Size AddressingMode AddressRegister - | MOVEMto Size AddressingMode "DataOrAddressRegister list" - | MOVEMfrom Size "DataOrAddressRegister list" AddressingMode - | MOVEP Size AddressingMode AddressingMode - | MOVEQ nat DataRegister - | MULS AddressingMode DataRegister - | MULU AddressingMode DataRegister - | NBCD AddressingMode - | NEG Size AddressingMode - | NEGX Size AddressingMode - | NOP - | NOT Size AddressingMode - | OR Size AddressingMode AddressingMode - | ORI Size nat AddressingMode - | ORItoCCR nat - | ORItoSR nat - | PEA AddressingMode - | RESET - | ROL Size AddressingMode DataRegister - | ROLW AddressingMode - | ROR Size AddressingMode DataRegister - | RORW AddressingMode - | ROXL Size AddressingMode DataRegister - | ROXLW AddressingMode - | ROXR Size AddressingMode DataRegister - | ROXRW AddressingMode - | RTE - | RTR - | RTS - | SBCD AddressingMode AddressingMode - | ST AddressingMode - | SF AddressingMode - | Scc Condition AddressingMode - | STOP nat - | SUB Size AddressingMode AddressingMode - | SUBA Size AddressingMode AddressingMode - | SUBI Size nat AddressingMode - | SUBQ Size nat AddressingMode - | SUBX Size AddressingMode AddressingMode - | SWAP DataRegister - | TAS AddressingMode - | TRAP nat - | TRAPV - | TST Size AddressingMode - | UNLK AddressRegister +old_datatype M68kInstruction = + ABCD AddressingMode AddressingMode +| ADD Size AddressingMode AddressingMode +| ADDA Size AddressingMode AddressRegister +| ADDI Size nat AddressingMode +| ADDQ Size nat AddressingMode +| ADDX Size AddressingMode AddressingMode +| AND Size AddressingMode AddressingMode +| ANDI Size nat AddressingMode +| ANDItoCCR nat +| ANDItoSR nat +| ASL Size AddressingMode DataRegister +| ASLW AddressingMode +| ASR Size AddressingMode DataRegister +| ASRW AddressingMode +| Bcc Condition Size nat +| BTST Size AddressingMode AddressingMode +| BCHG Size AddressingMode AddressingMode +| BCLR Size AddressingMode AddressingMode +| BSET Size AddressingMode AddressingMode +| BRA Size nat +| BSR Size nat +| CHK AddressingMode DataRegister +| CLR Size AddressingMode +| CMP Size AddressingMode DataRegister +| CMPA Size AddressingMode AddressRegister +| CMPI Size nat AddressingMode +| CMPM Size AddressRegister AddressRegister +| DBT DataRegister nat +| DBF DataRegister nat +| DBcc Condition DataRegister nat +| DIVS AddressingMode DataRegister +| DIVU AddressingMode DataRegister +| EOR Size DataRegister AddressingMode +| EORI Size nat AddressingMode +| EORItoCCR nat +| EORItoSR nat +| EXG DataOrAddressRegister DataOrAddressRegister +| EXT Size DataRegister +| ILLEGAL +| JMP AddressingMode +| JSR AddressingMode +| LEA AddressingMode AddressRegister +| LINK AddressRegister nat +| LSL Size AddressingMode DataRegister +| LSLW AddressingMode +| LSR Size AddressingMode DataRegister +| LSRW AddressingMode +| MOVE Size AddressingMode AddressingMode +| MOVEtoCCR AddressingMode +| MOVEtoSR AddressingMode +| MOVEfromSR AddressingMode +| MOVEtoUSP AddressingMode +| MOVEfromUSP AddressingMode +| MOVEA Size AddressingMode AddressRegister +| MOVEMto Size AddressingMode "DataOrAddressRegister list" +| MOVEMfrom Size "DataOrAddressRegister list" AddressingMode +| MOVEP Size AddressingMode AddressingMode +| MOVEQ nat DataRegister +| MULS AddressingMode DataRegister +| MULU AddressingMode DataRegister +| NBCD AddressingMode +| NEG Size AddressingMode +| NEGX Size AddressingMode +| NOP +| NOT Size AddressingMode +| OR Size AddressingMode AddressingMode +| ORI Size nat AddressingMode +| ORItoCCR nat +| ORItoSR nat +| PEA AddressingMode +| RESET +| ROL Size AddressingMode DataRegister +| ROLW AddressingMode +| ROR Size AddressingMode DataRegister +| RORW AddressingMode +| ROXL Size AddressingMode DataRegister +| ROXLW AddressingMode +| ROXR Size AddressingMode DataRegister +| ROXRW AddressingMode +| RTE +| RTR +| RTS +| SBCD AddressingMode AddressingMode +| ST AddressingMode +| SF AddressingMode +| Scc Condition AddressingMode +| STOP nat +| SUB Size AddressingMode AddressingMode +| SUBA Size AddressingMode AddressingMode +| SUBI Size nat AddressingMode +| SUBQ Size nat AddressingMode +| SUBX Size AddressingMode AddressingMode +| SWAP DataRegister +| TAS AddressingMode +| TRAP nat +| TRAPV +| TST Size AddressingMode +| UNLK AddressRegister end diff -r acc2f1801acc -r 57752a91eec4 src/HOL/Fun_Def.thy --- a/src/HOL/Fun_Def.thy Thu Sep 11 18:54:36 2014 +0200 +++ b/src/HOL/Fun_Def.thy Thu Sep 11 18:54:36 2014 +0200 @@ -97,7 +97,7 @@ method_setup pat_completeness = {* Scan.succeed (SIMPLE_METHOD' o Pat_Completeness.pat_completeness_tac) -*} "prove completeness of datatype patterns" +*} "prove completeness of (co)datatype patterns" ML_file "Tools/Function/fun.ML" ML_file "Tools/Function/induction_schema.ML" diff -r acc2f1801acc -r 57752a91eec4 src/HOL/HOLCF/FOCUS/Buffer.thy --- a/src/HOL/HOLCF/FOCUS/Buffer.thy Thu Sep 11 18:54:36 2014 +0200 +++ b/src/HOL/HOLCF/FOCUS/Buffer.thy Thu Sep 11 18:54:36 2014 +0200 @@ -25,12 +25,10 @@ typedecl D -datatype - +datatype_new M = Md D | Mreq ("\") -datatype - +datatype_new State = Sd D | Snil ("\") type_synonym diff -r acc2f1801acc -r 57752a91eec4 src/HOL/Hoare/Hoare_Logic.thy --- a/src/HOL/Hoare/Hoare_Logic.thy Thu Sep 11 18:54:36 2014 +0200 +++ b/src/HOL/Hoare/Hoare_Logic.thy Thu Sep 11 18:54:36 2014 +0200 @@ -15,11 +15,11 @@ type_synonym 'a bexp = "'a set" type_synonym 'a assn = "'a set" -datatype - 'a com = Basic "'a \ 'a" - | Seq "'a com" "'a com" ("(_;/ _)" [61,60] 60) - | Cond "'a bexp" "'a com" "'a com" ("(1IF _/ THEN _ / ELSE _/ FI)" [0,0,0] 61) - | While "'a bexp" "'a assn" "'a com" ("(1WHILE _/ INV {_} //DO _ /OD)" [0,0,0] 61) +datatype_new 'a com = + Basic "'a \ 'a" +| Seq "'a com" "'a com" ("(_;/ _)" [61,60] 60) +| Cond "'a bexp" "'a com" "'a com" ("(1IF _/ THEN _ / ELSE _/ FI)" [0,0,0] 61) +| While "'a bexp" "'a assn" "'a com" ("(1WHILE _/ INV {_} //DO _ /OD)" [0,0,0] 61) abbreviation annskip ("SKIP") where "SKIP == Basic id" diff -r acc2f1801acc -r 57752a91eec4 src/HOL/Hoare/Hoare_Logic_Abort.thy --- a/src/HOL/Hoare/Hoare_Logic_Abort.thy Thu Sep 11 18:54:36 2014 +0200 +++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy Thu Sep 11 18:54:36 2014 +0200 @@ -12,12 +12,12 @@ type_synonym 'a bexp = "'a set" type_synonym 'a assn = "'a set" -datatype - 'a com = Basic "'a \ 'a" - | Abort - | Seq "'a com" "'a com" ("(_;/ _)" [61,60] 60) - | Cond "'a bexp" "'a com" "'a com" ("(1IF _/ THEN _ / ELSE _/ FI)" [0,0,0] 61) - | While "'a bexp" "'a assn" "'a com" ("(1WHILE _/ INV {_} //DO _ /OD)" [0,0,0] 61) +datatype_new 'a com = + Basic "'a \ 'a" +| Abort +| Seq "'a com" "'a com" ("(_;/ _)" [61,60] 60) +| Cond "'a bexp" "'a com" "'a com" ("(1IF _/ THEN _ / ELSE _/ FI)" [0,0,0] 61) +| While "'a bexp" "'a assn" "'a com" ("(1WHILE _/ INV {_} //DO _ /OD)" [0,0,0] 61) abbreviation annskip ("SKIP") where "SKIP == Basic id" diff -r acc2f1801acc -r 57752a91eec4 src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy Thu Sep 11 18:54:36 2014 +0200 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy Thu Sep 11 18:54:36 2014 +0200 @@ -37,7 +37,7 @@ and filter_less': "filter_less' (n1 n1 <: a1 \ n2 <: a2 \ n1 <: a1' \ n2 <: a2'" -datatype 'a up = bot | Up 'a +old_datatype 'a up = bot | Up 'a instantiation up :: (SL_top)SL_top begin diff -r acc2f1801acc -r 57752a91eec4 src/HOL/IMP/Com.thy --- a/src/HOL/IMP/Com.thy Thu Sep 11 18:54:36 2014 +0200 +++ b/src/HOL/IMP/Com.thy Thu Sep 11 18:54:36 2014 +0200 @@ -2,7 +2,7 @@ theory Com imports BExp begin -datatype +datatype_new com = SKIP | Assign vname aexp ("_ ::= _" [1000, 61] 61) | Seq com com ("_;;/ _" [60, 61] 60) diff -r acc2f1801acc -r 57752a91eec4 src/HOL/IMP/Procs.thy --- a/src/HOL/IMP/Procs.thy Thu Sep 11 18:54:36 2014 +0200 +++ b/src/HOL/IMP/Procs.thy Thu Sep 11 18:54:36 2014 +0200 @@ -6,7 +6,7 @@ type_synonym pname = string -datatype +datatype_new com = SKIP | Assign vname aexp ("_ ::= _" [1000, 61] 61) | Seq com com ("_;;/ _" [60, 61] 60) diff -r acc2f1801acc -r 57752a91eec4 src/HOL/Imperative_HOL/Heap.thy --- a/src/HOL/Imperative_HOL/Heap.thy Thu Sep 11 18:54:36 2014 +0200 +++ b/src/HOL/Imperative_HOL/Heap.thy Thu Sep 11 18:54:36 2014 +0200 @@ -53,11 +53,8 @@ definition empty :: heap where "empty = \arrays = (\_ _. []), refs = (\_ _. 0), lim = 0\" -datatype_new 'a array = Array addr -- "note the phantom type 'a" -datatype_compat array - -datatype_new 'a ref = Ref addr -- "note the phantom type 'a" -datatype_compat ref +old_datatype 'a array = Array addr -- "note the phantom type 'a" +old_datatype 'a ref = Ref addr -- "note the phantom type 'a" primrec addr_of_array :: "'a array \ addr" where "addr_of_array (Array x) = x" diff -r acc2f1801acc -r 57752a91eec4 src/HOL/Imperative_HOL/ex/Linked_Lists.thy --- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Thu Sep 11 18:54:36 2014 +0200 +++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Thu Sep 11 18:54:36 2014 +0200 @@ -11,7 +11,7 @@ section {* Definition of Linked Lists *} setup {* Sign.add_const_constraint (@{const_name Ref}, SOME @{typ "nat \ 'a\type ref"}) *} -datatype 'a node = Empty | Node 'a "'a node ref" +old_datatype 'a node = Empty | Node 'a "'a node ref" primrec node_encode :: "'a\countable node \ nat" diff -r acc2f1801acc -r 57752a91eec4 src/HOL/Induct/Com.thy --- a/src/HOL/Induct/Com.thy Thu Sep 11 18:54:36 2014 +0200 +++ b/src/HOL/Induct/Com.thy Thu Sep 11 18:54:36 2014 +0200 @@ -12,7 +12,7 @@ typedecl loc type_synonym state = "loc => nat" -datatype +datatype_new exp = N nat | X loc | Op "nat => nat => nat" exp exp diff -r acc2f1801acc -r 57752a91eec4 src/HOL/Induct/QuoDataType.thy --- a/src/HOL/Induct/QuoDataType.thy Thu Sep 11 18:54:36 2014 +0200 +++ b/src/HOL/Induct/QuoDataType.thy Thu Sep 11 18:54:36 2014 +0200 @@ -10,7 +10,7 @@ subsection{*Defining the Free Algebra*} text{*Messages with encryption and decryption as free constructors.*} -datatype +datatype_new freemsg = NONCE nat | MPAIR freemsg freemsg | CRYPT nat freemsg diff -r acc2f1801acc -r 57752a91eec4 src/HOL/Induct/QuoNestedDataType.thy --- a/src/HOL/Induct/QuoNestedDataType.thy Thu Sep 11 18:54:36 2014 +0200 +++ b/src/HOL/Induct/QuoNestedDataType.thy Thu Sep 11 18:54:36 2014 +0200 @@ -10,11 +10,13 @@ subsection{*Defining the Free Algebra*} text{*Messages with encryption and decryption as free constructors.*} -datatype +datatype_new freeExp = VAR nat | PLUS freeExp freeExp | FNCALL nat "freeExp list" +datatype_compat freeExp + text{*The equivalence relation, which makes PLUS associative.*} text{*The first rule is the desired equation. The next three rules @@ -38,7 +40,8 @@ lemma exprel_refl: "X \ X" and list_exprel_refl: "(Xs,Xs) \ listrel(exprel)" - by (induct X and Xs) (blast intro: exprel.intros listrel.intros)+ + by (induct X and Xs rule: compat_freeExp.induct compat_freeExp_list.induct) + (blast intro: exprel.intros listrel.intros)+ theorem equiv_exprel: "equiv UNIV exprel" proof - @@ -306,7 +309,7 @@ lemma vars_FnCall [simp]: "vars (FnCall F Xs) = vars_list Xs" apply (cases Xs rule: eq_Abs_ExpList) apply (simp add: FnCall) -apply (induct_tac Us) +apply (induct_tac Us) apply (simp_all add: vars_def UN_equiv_class [OF equiv_exprel vars_respects]) done @@ -428,7 +431,7 @@ obtain U where exp: "exp = (Abs_Exp (exprel `` {U}))" by (cases exp) obtain Us where list: "list = Abs_ExpList Us" by (rule eq_Abs_ExpList) have "P1 (Abs_Exp (exprel `` {U}))" and "P2 (Abs_ExpList Us)" - proof (induct U and Us) + proof (induct U and Us rule: compat_freeExp.induct compat_freeExp_list.induct) case (VAR nat) with V show ?case by (simp add: Var_def) next diff -r acc2f1801acc -r 57752a91eec4 src/HOL/Induct/SList.thy --- a/src/HOL/Induct/SList.thy Thu Sep 11 18:54:36 2014 +0200 +++ b/src/HOL/Induct/SList.thy Thu Sep 11 18:54:36 2014 +0200 @@ -15,10 +15,10 @@ so that list can serve as a "functor" for defining other recursive types. -This enables the conservative construction of mutual recursive data-types +This enables the conservative construction of mutual recursive datatypes such as -datatype 'a m = Node 'a * ('a m) list +datatype 'a m = Node 'a * 'a m list *) header {* Extended List Theory (old) *} diff -r acc2f1801acc -r 57752a91eec4 src/HOL/Nominal/Examples/Fsub.thy --- a/src/HOL/Nominal/Examples/Fsub.thy Thu Sep 11 18:54:36 2014 +0200 +++ b/src/HOL/Nominal/Examples/Fsub.thy Thu Sep 11 18:54:36 2014 +0200 @@ -30,7 +30,7 @@ there are infinitely many elements in @{text "tyvrs"} and @{text "vrs"}. *} text{* The constructors for types and terms in System \FSUB{} contain abstractions - over type-variables and term-variables. The nominal datatype-package uses + over type-variables and term-variables. The nominal datatype package uses @{text "\\\\"} to indicate where abstractions occur. *} nominal_datatype ty = diff -r acc2f1801acc -r 57752a91eec4 src/HOL/Old_Datatype.thy --- a/src/HOL/Old_Datatype.thy Thu Sep 11 18:54:36 2014 +0200 +++ b/src/HOL/Old_Datatype.thy Thu Sep 11 18:54:36 2014 +0200 @@ -7,7 +7,7 @@ theory Old_Datatype imports Power -keywords "datatype" :: thy_decl +keywords "old_datatype" :: thy_decl begin subsection {* The datatype universe *} diff -r acc2f1801acc -r 57752a91eec4 src/HOL/Quotient_Examples/Quotient_Message.thy --- a/src/HOL/Quotient_Examples/Quotient_Message.thy Thu Sep 11 18:54:36 2014 +0200 +++ b/src/HOL/Quotient_Examples/Quotient_Message.thy Thu Sep 11 18:54:36 2014 +0200 @@ -10,7 +10,7 @@ subsection{*Defining the Free Algebra*} -datatype +datatype_new freemsg = NONCE nat | MPAIR freemsg freemsg | CRYPT nat freemsg diff -r acc2f1801acc -r 57752a91eec4 src/HOL/SET_Protocol/Event_SET.thy --- a/src/HOL/SET_Protocol/Event_SET.thy Thu Sep 11 18:54:36 2014 +0200 +++ b/src/HOL/SET_Protocol/Event_SET.thy Thu Sep 11 18:54:36 2014 +0200 @@ -15,7 +15,7 @@ text{*Message events*} -datatype +datatype_new event = Says agent agent msg | Gets agent msg | Notes agent msg diff -r acc2f1801acc -r 57752a91eec4 src/HOL/SET_Protocol/Message_SET.thy --- a/src/HOL/SET_Protocol/Message_SET.thy Thu Sep 11 18:54:36 2014 +0200 +++ b/src/HOL/SET_Protocol/Message_SET.thy Thu Sep 11 18:54:36 2014 +0200 @@ -52,11 +52,11 @@ text{*Agents. We allow any number of certification authorities, cardholders merchants, and payment gateways.*} -datatype +datatype_new agent = CA nat | Cardholder nat | Merchant nat | PG nat | Spy text{*Messages*} -datatype +datatype_new msg = Agent agent --{*Agent names*} | Number nat --{*Ordinary integers, timestamps, ...*} | Nonce nat --{*Unguessable nonces*} @@ -373,6 +373,7 @@ (*MPair case: blast_tac works out the necessary sum itself!*) prefer 2 apply (blast elim!: add_leE) (*Nonce case*) +apply (rename_tac nat) apply (rule_tac x = "N + Suc nat" in exI) apply (auto elim!: add_leE) done @@ -382,6 +383,7 @@ apply (induct_tac "msg") apply (simp_all (no_asm_simp) add: exI parts_insert2) prefer 2 apply (blast elim!: add_leE) +apply (rename_tac nat) apply (rule_tac x = "N + Suc nat" in exI, auto) done diff -r acc2f1801acc -r 57752a91eec4 src/HOL/Tools/BNF/bnf_lfp.ML --- a/src/HOL/Tools/BNF/bnf_lfp.ML Thu Sep 11 18:54:36 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML Thu Sep 11 18:54:36 2014 +0200 @@ -1814,6 +1814,10 @@ end; val _ = + Outer_Syntax.local_theory @{command_spec "datatype"} "define inductive datatypes" + (parse_co_datatype_cmd Least_FP construct_lfp); + +val _ = Outer_Syntax.local_theory @{command_spec "datatype_new"} "define inductive datatypes" (parse_co_datatype_cmd Least_FP construct_lfp); diff -r acc2f1801acc -r 57752a91eec4 src/HOL/Tools/Old_Datatype/old_datatype.ML --- a/src/HOL/Tools/Old_Datatype/old_datatype.ML Thu Sep 11 18:54:36 2014 +0200 +++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML Thu Sep 11 18:54:36 2014 +0200 @@ -791,7 +791,7 @@ >> (fn (((vs, t), mx), cons) => ((t, vs, mx), map Parse.triple1 cons)); val _ = - Outer_Syntax.command @{command_spec "datatype"} "define old-style inductive datatypes" + Outer_Syntax.command @{command_spec "old_datatype"} "define old-style inductive datatypes" (Parse.and_list1 spec_cmd >> (Toplevel.theory o (snd oo add_datatype_cmd Old_Datatype_Aux.default_config))); diff -r acc2f1801acc -r 57752a91eec4 src/HOL/ex/Reflection_Examples.thy --- a/src/HOL/ex/Reflection_Examples.thy Thu Sep 11 18:54:36 2014 +0200 +++ b/src/HOL/ex/Reflection_Examples.thy Thu Sep 11 18:54:36 2014 +0200 @@ -17,7 +17,7 @@ often need its structure. Traditionnaly such simplifications are written in ML, proofs are synthesized. -An other strategy is to declare an HOL-datatype @{text \} and an HOL function (the +An other strategy is to declare an HOL datatype @{text \} and an HOL function (the interpretation) that maps elements of @{text \} to elements of @{text \}. The functionality of @{text reify} then is, given a term @{text t} of type @{text \}, diff -r acc2f1801acc -r 57752a91eec4 src/HOL/ex/Refute_Examples.thy --- a/src/HOL/ex/Refute_Examples.thy Thu Sep 11 18:54:36 2014 +0200 +++ b/src/HOL/ex/Refute_Examples.thy Thu Sep 11 18:54:36 2014 +0200 @@ -507,10 +507,6 @@ subsubsection {* Inductive datatypes *} -text {* With @{text quick_and_dirty} set, the datatype package does - not generate certain axioms for recursion operators. Without these - axioms, Refute may find spurious countermodels. *} - text {* unit *} lemma "P (x::unit)"