
diff -r 6e2479089226 -r cecd7a941885 ProgTutorial/Package/Ind_Interface.thy
--- a/ProgTutorial/Package/Ind_Interface.thy	Tue May 14 16:59:53 2019 +0200
+++ b/ProgTutorial/Package/Ind_Interface.thy	Tue May 14 17:10:47 2019 +0200
@@ -3,13 +3,13 @@
 keywords "simple_inductive2" :: thy_decl
 begin
 
-section {* Parsing and Typing the Specification\label{sec:interface} *}
+section \<open>Parsing and Typing the Specification\label{sec:interface}\<close>
 
-text_raw {*
+text_raw \<open>
 \begin{figure}[t]
 \begin{boxedminipage}{\textwidth}
 \begin{isabelle}
-*}
+\<close>
 simple_inductive
   trcl :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
 where
@@ -42,16 +42,16 @@
 | fresh_app: "\<lbrakk>fresh a t; fresh a s\<rbrakk> \<Longrightarrow> fresh a (App t s)"
 | fresh_lam1: "fresh a (Lam a t)"
 | fresh_lam2: "\<lbrakk>a\<noteq>b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"
-text_raw {*
+text_raw \<open>
 \end{isabelle}
 \end{boxedminipage}
 \caption{Specification given by the user for the inductive predicates
 @{term "trcl"}, @{term "even"} and @{term "odd"}, @{term "accpart"} and 
 @{term "fresh"}.\label{fig:specs}}
 \end{figure}  
-*}
+\<close>
 
-text {* 
+text \<open>
   To be able to write down the specifications of inductive predicates, we have
   to introduce a new command (see Section~\ref{sec:newcommand}).  As the
   keyword for the new command we chose \simpleinductive{}. Examples of
@@ -59,31 +59,31 @@
   Figure~\ref{fig:specs}. The syntax used in these examples more or
   less translates directly into the parser:
 
-*}
+\<close>
 
-ML %grayML{*val spec_parser = 
+ML %grayML\<open>val spec_parser = 
    Parse.vars -- 
    Scan.optional 
      (Parse.$$$ "where" |--
         Parse.!!! 
           (Parse.enum1 "|" 
-             (Parse_Spec.opt_thm_name ":" -- Parse.prop))) []*}
+             (Parse_Spec.opt_thm_name ":" -- Parse.prop))) []\<close>
 
-text {*
+text \<open>
   which we explained in Section~\ref{sec:parsingspecs}.  There is no code included 
   for parsing the keyword and what is called a \emph{target}. The latter  can be given 
   optionally after the keyword. The target is an ``advanced'' feature which we will 
   inherit for ``free'' from the infrastructure on which we shall build the package. 
   The target stands for a locale and allows us to specify
-*}
+\<close>
 
 locale rel =
   fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
 
-text {*
+text \<open>
   and then define the transitive closure and the accessible part of this 
   locale as follows:
-*}
+\<close>
 
 simple_inductive (in rel) 
   trcl' 
@@ -95,11 +95,11 @@
   accpart'
 where
   accpartI: "(\<And>y. R y x \<Longrightarrow> accpart' y) \<Longrightarrow> accpart' x"
-(*<*)ML %no{*fun filtered_input str = 
+(*<*)ML %no\<open>fun filtered_input str = 
   filter Token.is_proper (Token.explode (Thy_Header.get_keywords' @{context}) Position.none str) 
-fun parse p input = Scan.finite Token.stopper (Scan.error p) input*}(*>*)
-text {*
-  Note that in these definitions the parameter @{text R}, standing for the
+fun parse p input = Scan.finite Token.stopper (Scan.error p) input\<close>(*>*)
+text \<open>
+  Note that in these definitions the parameter \<open>R\<close>, standing for the
   relation, is left implicit. For the moment we will ignore this kind
   of implicit parameters and rely on the fact that the infrastructure will
   deal with them. Later, however, we will come back to them.
@@ -127,24 +127,24 @@
   and specifications of the introduction rules. This is all the information we
   need for calling the package and setting up the keyword. The latter is
   done in Lines 5 to 7 in the code below.
-*}
-(*<*)ML %no{*fun add_inductive_cmd pred_specs rule_specs lthy = lthy 
-   fun add_inductive pred_specs rule_specs lthy = lthy*}(*>*) (* FIXME: Is the dummy simple_inductive2 installed with ML, before there was ML_val*)
-ML %linenosgray{*val specification : (local_theory -> local_theory) parser =
+\<close>
+(*<*)ML %no\<open>fun add_inductive_cmd pred_specs rule_specs lthy = lthy 
+   fun add_inductive pred_specs rule_specs lthy = lthy\<close>(*>*) (* FIXME: Is the dummy simple_inductive2 installed with ML, before there was ML_val*)
+ML %linenosgray\<open>val specification : (local_theory -> local_theory) parser =
   spec_parser >>
     (fn (pred_specs, rule_specs) => add_inductive_cmd pred_specs rule_specs)
 
 val _ = Outer_Syntax.local_theory @{command_keyword "simple_inductive2"}
           "definition of simple inductive predicates"
-             specification*}
+             specification\<close>
 
-text {*
+text \<open>
   We call @{ML_ind  local_theory in Outer_Syntax} with the kind-indicator 
   @{ML_ind  thy_decl in Keyword} since the package does not need to open 
   up any proof (see Section~\ref{sec:newcommand}). 
-  The auxiliary function @{text specification} in Lines 1 to 3
+  The auxiliary function \<open>specification\<close> in Lines 1 to 3
   gathers the information from the parser to be processed further
-  by the function @{text "add_inductive_cmd"}, which we describe below. 
+  by the function \<open>add_inductive_cmd\<close>, which we describe below. 
 
   Note that the predicates when they come out of the parser are just some
   ``naked'' strings: they have no type yet (even if we annotate them with
@@ -158,23 +158,23 @@
   user and the type constraints by the ``ambient'' theory. It returns 
   the type for the predicates and also returns typed terms for the
   introduction rules. So at the heart of the function 
-  @{text "add_inductive_cmd"} is a call to @{ML read_multi_specs in Specification}.
-*}
+  \<open>add_inductive_cmd\<close> is a call to @{ML read_multi_specs in Specification}.
+\<close>
 
-ML_val%grayML{*fun add_inductive_cmd pred_specs rule_specs lthy =
+ML_val%grayML\<open>fun add_inductive_cmd pred_specs rule_specs lthy =
 let
   val ((pred_specs', rule_specs'), _) = 
          Specification.read_multi_specs pred_specs rule_specs lthy
 in
   add_inductive pred_specs' rule_specs' lthy
-end*}
+end\<close>
 
-text {*
+text \<open>
   Once we have the input data as some internal datastructure, we call
-  the function @{text add_inductive}. This function does the  heavy duty 
+  the function \<open>add_inductive\<close>. This function does the  heavy duty 
   lifting in the package: it generates definitions for the 
   predicates and derives from them corresponding induction principles and 
   introduction rules. The description of this function will span over
   the next two sections.
-*}
+\<close>
 (*<*)end(*>*)




