--- a/ProgTutorial/Package/Ind_Extensions.thy	Tue May 14 16:59:53 2019 +0200
+++ b/ProgTutorial/Package/Ind_Extensions.thy	Tue May 14 17:10:47 2019 +0200
@@ -2,7 +2,7 @@
 imports Simple_Inductive_Package Ind_Intro
 begin
 
-section {* Extensions of the Package (TBD) *}
+section \<open>Extensions of the Package (TBD)\<close>
 
 (*
 text {*
@@ -29,7 +29,7 @@
 *}
 *)
 
-text {*
+text \<open>
   Things to include at the end:
 
   \begin{itemize}
@@ -39,7 +39,7 @@
   \item say something about the two interfaces for calling packages
   \end{itemize}
   
-*}
+\<close>
 
 (*
 simple_inductive
@@ -129,32 +129,32 @@
   accpartI: "(\<And>y. R y x \<Longrightarrow> accpart'' R y) \<Longrightarrow> accpart'' R x"
 *)
 
-text {*
+text \<open>
   \begin{exercise}
   In Section~\ref{sec:nutshell} we required that introduction rules must be of the
   form
 
   \begin{isabelle}
-  @{text "rule ::= \<And>xs. As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^sup>* \<Longrightarrow> pred ts"}
+  \<open>rule ::= \<And>xs. As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^sup>* \<Longrightarrow> pred ts\<close>
   \end{isabelle}
 
-  where the @{text "As"} and @{text "Bs"} can be any collection of formulae
-  not containing the @{text "preds"}. This requirement is important,
+  where the \<open>As\<close> and \<open>Bs\<close> can be any collection of formulae
+  not containing the \<open>preds\<close>. This requirement is important,
   because if violated, the theory behind the inductive package does not work
   and also the proofs break. Write code that tests whether the introduction
   rules given by the user fit into the scheme described above. Hint: It 
   is not important in which order the premises ar given; the
-  @{text "As"} and @{text "(\<And>ys. Bs \<Longrightarrow> pred ss)"} premises can occur
+  \<open>As\<close> and \<open>(\<And>ys. Bs \<Longrightarrow> pred ss)\<close> premises can occur
   in any order.
   \end{exercise}
-*}  
+\<close>  
 
-text_raw {*
+text_raw \<open>
   \begin{exercise}
-  If you define @{text even} and @{text odd} with the standard inductive
+  If you define \<open>even\<close> and \<open>odd\<close> with the standard inductive
   package
   \begin{isabelle}
-*}
+\<close>
 inductive 
   even_2 and odd_2
 where
@@ -162,11 +162,11 @@
 | evenS_2: "odd_2 m \<Longrightarrow> even_2 (Suc m)"
 | oddS_2:  "even_2 m \<Longrightarrow> odd_2 (Suc m)"
 
-text_raw{*
+text_raw\<open>
   \end{isabelle}
 
-  you will see that the generated induction principle for @{text "even'"} (namely
-  @{text "even_2_odd_2.inducts"} has the additional assumptions 
+  you will see that the generated induction principle for \<open>even'\<close> (namely
+  \<open>even_2_odd_2.inducts\<close> has the additional assumptions 
   @{prop "odd_2 m"} and @{prop "even_2 m"} in the recursive cases. These additional 
   assumptions can sometimes make ``life easier'' in proofs. Since 
   more assumptions can be made when proving properties, these induction principles 
@@ -186,29 +186,29 @@
   provides a richer reasoning infrastructure. The code of this package can be found in 
   @{ML_file "HOL/Tools/inductive.ML"}.
   \end{readmore}
-*}
+\<close>
 
-section {* Definitional Packages *}
+section \<open>Definitional Packages\<close>
 
-text {* Type declarations *}
+text \<open>Type declarations\<close>
 
 (*
 ML %grayML{*Typedef.add_typedef_global (@{binding test}, [], NoSyn)
   @{term "{1}::nat set"} NONE (simp_tac @{context} 1) @{theory} *}
 *)
 
-ML %grayML{*fun pat_completeness_auto ctxt =
+ML %grayML\<open>fun pat_completeness_auto ctxt =
   Pat_Completeness.pat_completeness_tac ctxt 1
-    THEN auto_tac ctxt*}
+    THEN auto_tac ctxt\<close>
 
-ML {*
+ML \<open>
   val conf = Function_Common.default_config
-*}
+\<close>
 
 datatype foo = Foo nat
 
-local_setup{*Function.add_function [(@{binding "baz"}, NONE, NoSyn)] 
+local_setup\<open>Function.add_function [(@{binding "baz"}, NONE, NoSyn)] 
     [((Binding.empty_atts,@{term "\<And>x. baz (Foo x) = x"}),[],[])]
-      conf pat_completeness_auto #> snd*}
+      conf pat_completeness_auto #> snd\<close>
 
 (*<*)end(*>*)