1.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy	Tue Jun 12 10:25:27 2018 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy	Tue Jun 12 14:53:47 2018 +0200
     1.3 @@ -274,6 +274,8 @@
     1.4    no_met :: ID  make_ratpoly_in :: ID          
     1.5    bdv :: real  c :: real  c_2 :: real  c_3 :: real  c_4 :: real
     1.6  
     1.7 +BETTER see HOL/ex/Cartouche_Examples.thy subsection \<open>Inner syntax: string literals via cartouche\<close>
     1.8 +
     1.9  partial_function (tailrec) biegelinie ::
    1.10    "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool list \<Rightarrow> bool"
    1.11  where