# HG changeset patch # User wenzelm # Date 1230841813 -3600 # Node ID 62e0f892e525b214c0ed7c86ff89a906490be78d # Parent 96cf8edb62494c2d5f28631c3c246a1b83f12594 updated generated files; diff -r 96cf8edb6249 -r 62e0f892e525 doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex --- a/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex Thu Jan 01 21:28:38 2009 +0100 +++ b/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex Thu Jan 01 21:30:13 2009 +0100 @@ -681,8 +681,8 @@ % \isatagquote \isacommand{interpretation}\isamarkupfalse% -\ idem{\isacharunderscore}class{\isacharcolon}\isanewline -\ \ idem\ {\isacharbrackleft}{\isachardoublequoteopen}f\ {\isasymColon}\ {\isacharparenleft}{\isasymalpha}{\isasymColon}idem{\isacharparenright}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}{\isacharbrackright}\isanewline +\ idem{\isacharunderscore}class{\isacharprime}{\isacharcolon}\ \ \ \ \isanewline +\ \ idem\ {\isachardoublequoteopen}f\ {\isasymColon}\ {\isacharparenleft}{\isasymalpha}{\isasymColon}idem{\isacharparenright}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\isanewline \isacommand{proof}\isamarkupfalse% \ \isacommand{qed}\isamarkupfalse% \ {\isacharparenleft}rule\ idem{\isacharparenright}% @@ -843,7 +843,7 @@ \endisadelimquote % \isatagquote -\isacommand{interpretation}\isamarkupfalse% +\isacommand{class{\isacharunderscore}interpretation}\isamarkupfalse% \ list{\isacharunderscore}monoid{\isacharcolon}\ monoid\ {\isacharbrackleft}append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline \ \ \isacommand{proof}\isamarkupfalse% \ \isacommand{qed}\isamarkupfalse% @@ -874,12 +874,12 @@ \ \ {\isachardoublequoteopen}replicate\ {\isadigit{0}}\ {\isacharunderscore}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline \ \ {\isacharbar}\ {\isachardoublequoteopen}replicate\ {\isacharparenleft}Suc\ n{\isacharparenright}\ xs\ {\isacharequal}\ xs\ {\isacharat}\ replicate\ n\ xs{\isachardoublequoteclose}\isanewline \isanewline -\isacommand{interpretation}\isamarkupfalse% +\isacommand{class{\isacharunderscore}interpretation}\isamarkupfalse% \ list{\isacharunderscore}monoid{\isacharcolon}\ monoid\ {\isacharbrackleft}append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\ \isakeyword{where}\isanewline \ \ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ append\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ replicate{\isachardoublequoteclose}\isanewline \isacommand{proof}\isamarkupfalse% \ {\isacharminus}\isanewline -\ \ \isacommand{interpret}\isamarkupfalse% +\ \ \isacommand{class{\isacharunderscore}interpret}\isamarkupfalse% \ monoid\ {\isacharbrackleft}append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% \isanewline \ \ \isacommand{show}\isamarkupfalse% @@ -1231,7 +1231,7 @@ \hspace*{0pt}\\ \hspace*{0pt}fun inverse{\char95}int i = IntInf.{\char126}~i;\\ \hspace*{0pt}\\ -\hspace*{0pt}val neutral{\char95}int :~IntInf.int = (0 :~IntInf.int);\\ +\hspace*{0pt}val neutral{\char95}int :~IntInf.int = (0 :~IntInf.int)\\ \hspace*{0pt}\\ \hspace*{0pt}fun mult{\char95}int i j = IntInf.+ (i,~j);\\ \hspace*{0pt}\\ @@ -1258,7 +1258,7 @@ \hspace*{0pt} ~~~else inverse A{\char95}~(pow{\char95}nat (monoid{\char95}group A{\char95}) (nat (IntInf.{\char126}~k)) x));\\ \hspace*{0pt}\\ \hspace*{0pt}val example :~IntInf.int =\\ -\hspace*{0pt} ~pow{\char95}int group{\char95}int (10 :~IntInf.int) ({\char126}2 :~IntInf.int);\\ +\hspace*{0pt} ~pow{\char95}int group{\char95}int (10 :~IntInf.int) ({\char126}2 :~IntInf.int)\\ \hspace*{0pt}\\ \hspace*{0pt}end;~(*struct Example*)% \end{isamarkuptext}% diff -r 96cf8edb6249 -r 62e0f892e525 doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex Thu Jan 01 21:28:38 2009 +0100 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex Thu Jan 01 21:30:13 2009 +0100 @@ -281,9 +281,9 @@ \hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\ \hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = True;\\ \hspace*{0pt}\\ -\hspace*{0pt}fun in{\char95}interval (k, l) n = anda (less{\char95}eq{\char95}nat k n) (less{\char95}eq{\char95}nat n l);\\ +\hspace*{0pt}fun in{\char95}interval (k,~l) n = anda (less{\char95}eq{\char95}nat k n) (less{\char95}eq{\char95}nat n l);\\ \hspace*{0pt}\\ -\hspace*{0pt}end; (*struct Example*)% +\hspace*{0pt}end;~(*struct Example*)% \end{isamarkuptext}% \isamarkuptrue% % @@ -357,9 +357,9 @@ \hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\ \hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = true;\\ \hspace*{0pt}\\ -\hspace*{0pt}fun in{\char95}interval (k, l) n = (less{\char95}eq{\char95}nat k n) andalso (less{\char95}eq{\char95}nat n l);\\ +\hspace*{0pt}fun in{\char95}interval (k,~l) n = (less{\char95}eq{\char95}nat k n) andalso (less{\char95}eq{\char95}nat n l);\\ \hspace*{0pt}\\ -\hspace*{0pt}end; (*struct Example*)% +\hspace*{0pt}end;~(*struct Example*)% \end{isamarkuptext}% \isamarkuptrue% % @@ -414,9 +414,9 @@ \hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\ \hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = true;\\ \hspace*{0pt}\\ -\hspace*{0pt}fun in{\char95}interval (k, l) n = less{\char95}eq{\char95}nat k n andalso less{\char95}eq{\char95}nat n l;\\ +\hspace*{0pt}fun in{\char95}interval (k,~l) n = less{\char95}eq{\char95}nat k n andalso less{\char95}eq{\char95}nat n l;\\ \hspace*{0pt}\\ -\hspace*{0pt}end; (*struct Example*)% +\hspace*{0pt}end;~(*struct Example*)% \end{isamarkuptext}% \isamarkuptrue% % diff -r 96cf8edb6249 -r 62e0f892e525 doc-src/IsarAdvanced/Codegen/Thy/document/Introduction.tex --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Introduction.tex Thu Jan 01 21:28:38 2009 +0100 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Introduction.tex Thu Jan 01 21:30:13 2009 +0100 @@ -164,20 +164,20 @@ \hspace*{0pt}\\ \hspace*{0pt}datatype 'a queue = Queue of 'a list * 'a list;\\ \hspace*{0pt}\\ -\hspace*{0pt}val empty :~'a queue = Queue ([], []);\\ +\hspace*{0pt}val empty :~'a queue = Queue ([],~[])\\ \hspace*{0pt}\\ -\hspace*{0pt}fun dequeue (Queue ([], [])) = (NONE, Queue ([], []))\\ -\hspace*{0pt} ~| dequeue (Queue (xs, y ::~ys)) = (SOME y, Queue (xs, ys))\\ -\hspace*{0pt} ~| dequeue (Queue (v ::~va, [])) =\\ +\hspace*{0pt}fun dequeue (Queue ([],~[])) = (NONE,~Queue ([],~[]))\\ +\hspace*{0pt} ~| dequeue (Queue (xs,~y ::~ys)) = (SOME y,~Queue (xs,~ys))\\ +\hspace*{0pt} ~| dequeue (Queue (v ::~va,~[])) =\\ \hspace*{0pt} ~~~let\\ \hspace*{0pt} ~~~~~val y ::~ys = rev (v ::~va);\\ \hspace*{0pt} ~~~in\\ -\hspace*{0pt} ~~~~~(SOME y, Queue ([], ys))\\ +\hspace*{0pt} ~~~~~(SOME y,~Queue ([],~ys))\\ \hspace*{0pt} ~~~end;\\ \hspace*{0pt}\\ -\hspace*{0pt}fun enqueue x (Queue (xs, ys)) = Queue (x ::~xs, ys);\\ +\hspace*{0pt}fun enqueue x (Queue (xs,~ys)) = Queue (x ::~xs,~ys);\\ \hspace*{0pt}\\ -\hspace*{0pt}end; (*struct Example*)% +\hspace*{0pt}end;~(*struct Example*)% \end{isamarkuptext}% \isamarkuptrue% % @@ -233,31 +233,31 @@ \hspace*{0pt}module Example where {\char123}\\ \hspace*{0pt}\\ \hspace*{0pt}\\ -\hspace*{0pt}foldla ::~forall a b. (a -> b -> a) -> a -> [b] -> a;\\ +\hspace*{0pt}foldla ::~forall a b.~(a -> b -> a) -> a -> [b] -> a;\\ \hspace*{0pt}foldla f a [] = a;\\ \hspace*{0pt}foldla f a (x :~xs) = foldla f (f a x) xs;\\ \hspace*{0pt}\\ -\hspace*{0pt}rev ::~forall a. [a] -> [a];\\ +\hspace*{0pt}rev ::~forall a.~[a] -> [a];\\ \hspace*{0pt}rev xs = foldla ({\char92}~xsa x -> x :~xsa) [] xs;\\ \hspace*{0pt}\\ -\hspace*{0pt}list{\char95}case ::~forall t a. t -> (a -> [a] -> t) -> [a] -> t;\\ +\hspace*{0pt}list{\char95}case ::~forall t a.~t -> (a -> [a] -> t) -> [a] -> t;\\ \hspace*{0pt}list{\char95}case f1 f2 (a :~list) = f2 a list;\\ \hspace*{0pt}list{\char95}case f1 f2 [] = f1;\\ \hspace*{0pt}\\ \hspace*{0pt}data Queue a = Queue [a] [a];\\ \hspace*{0pt}\\ -\hspace*{0pt}empty ::~forall a. Queue a;\\ +\hspace*{0pt}empty ::~forall a.~Queue a;\\ \hspace*{0pt}empty = Queue [] [];\\ \hspace*{0pt}\\ -\hspace*{0pt}dequeue ::~forall a. Queue a -> (Maybe a, Queue a);\\ -\hspace*{0pt}dequeue (Queue [] []) = (Nothing, Queue [] []);\\ -\hspace*{0pt}dequeue (Queue xs (y :~ys)) = (Just y, Queue xs ys);\\ +\hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\ +\hspace*{0pt}dequeue (Queue [] []) = (Nothing,~Queue [] []);\\ +\hspace*{0pt}dequeue (Queue xs (y :~ys)) = (Just y,~Queue xs ys);\\ \hspace*{0pt}dequeue (Queue (v :~va) []) =\\ \hspace*{0pt} ~let {\char123}\\ \hspace*{0pt} ~~~(y :~ys) = rev (v :~va);\\ -\hspace*{0pt} ~{\char125}~in (Just y, Queue [] ys);\\ +\hspace*{0pt} ~{\char125}~in (Just y,~Queue [] ys);\\ \hspace*{0pt}\\ -\hspace*{0pt}enqueue ::~forall a. a -> Queue a -> Queue a;\\ +\hspace*{0pt}enqueue ::~forall a.~a -> Queue a -> Queue a;\\ \hspace*{0pt}enqueue x (Queue xs ys) = Queue (x :~xs) ys;\\ \hspace*{0pt}\\ \hspace*{0pt}{\char125}% diff -r 96cf8edb6249 -r 62e0f892e525 doc-src/IsarAdvanced/Codegen/Thy/document/ML.tex --- a/doc-src/IsarAdvanced/Codegen/Thy/document/ML.tex Thu Jan 01 21:28:38 2009 +0100 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/ML.tex Thu Jan 01 21:30:13 2009 +0100 @@ -54,9 +54,9 @@ \begin{mldecls} \indexml{Code.add\_eqn}\verb|Code.add_eqn: thm -> theory -> theory| \\ \indexml{Code.del\_eqn}\verb|Code.del_eqn: thm -> theory -> theory| \\ - \indexml{Code.add\_eqnl}\verb|Code.add_eqnl: string * (thm * bool) list Lazy.T -> theory -> theory| \\ - \indexml{Code.map\_pre}\verb|Code.map_pre: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory| \\ - \indexml{Code.map\_post}\verb|Code.map_post: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory| \\ + \indexml{Code.add\_eqnl}\verb|Code.add_eqnl: string * (thm * bool) list lazy -> theory -> theory| \\ + \indexml{Code.map\_pre}\verb|Code.map_pre: (simpset -> simpset) -> theory -> theory| \\ + \indexml{Code.map\_post}\verb|Code.map_post: (simpset -> simpset) -> theory -> theory| \\ \indexml{Code.add\_functrans}\verb|Code.add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option)|\isasep\isanewline% \verb| -> theory -> theory| \\ \indexml{Code.del\_functrans}\verb|Code.del_functrans: string -> theory -> theory| \\ @@ -126,7 +126,7 @@ \begin{mldecls} \indexml{Code\_Unit.read\_const}\verb|Code_Unit.read_const: theory -> string -> string| \\ \indexml{Code\_Unit.head\_eqn}\verb|Code_Unit.head_eqn: theory -> thm -> string * ((string * sort) list * typ)| \\ - \indexml{Code\_Unit.rewrite\_eqn}\verb|Code_Unit.rewrite_eqn: MetaSimplifier.simpset -> thm -> thm| \\ + \indexml{Code\_Unit.rewrite\_eqn}\verb|Code_Unit.rewrite_eqn: simpset -> thm -> thm| \\ \end{mldecls} \begin{description} diff -r 96cf8edb6249 -r 62e0f892e525 doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex Thu Jan 01 21:28:38 2009 +0100 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex Thu Jan 01 21:30:13 2009 +0100 @@ -87,10 +87,10 @@ \begin{isamarkuptext}% \isatypewriter% \noindent% -\hspace*{0pt}dequeue ::~forall a. Queue a -> (Maybe a, Queue a);\\ -\hspace*{0pt}dequeue (Queue xs (y :~ys)) = (Just y, Queue xs ys);\\ +\hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\ +\hspace*{0pt}dequeue (Queue xs (y :~ys)) = (Just y,~Queue xs ys);\\ \hspace*{0pt}dequeue (Queue xs []) =\\ -\hspace*{0pt} ~(if nulla xs then (Nothing, Queue [] [])\\ +\hspace*{0pt} ~(if nulla xs then (Nothing,~Queue [] [])\\ \hspace*{0pt} ~~~else dequeue (Queue [] (rev xs)));% \end{isamarkuptext}% \isamarkuptrue% @@ -286,7 +286,7 @@ \hspace*{0pt} ~neutral ::~a;\\ \hspace*{0pt}{\char125};\\ \hspace*{0pt}\\ -\hspace*{0pt}pow ::~forall a. (Monoid a) => Nat -> a -> a;\\ +\hspace*{0pt}pow ::~forall a.~(Monoid a) => Nat -> a -> a;\\ \hspace*{0pt}pow Zero{\char95}nat a = neutral;\\ \hspace*{0pt}pow (Suc n) a = mult a (pow n a);\\ \hspace*{0pt}\\ @@ -346,7 +346,7 @@ \hspace*{0pt}type 'a semigroup = {\char123}mult :~'a -> 'a -> 'a{\char125};\\ \hspace*{0pt}fun mult (A{\char95}:'a semigroup) = {\char35}mult A{\char95};\\ \hspace*{0pt}\\ -\hspace*{0pt}type 'a monoid = {\char123}Program{\char95}{\char95}semigroup{\char95}monoid :~'a semigroup, neutral :~'a{\char125};\\ +\hspace*{0pt}type 'a monoid = {\char123}Program{\char95}{\char95}semigroup{\char95}monoid :~'a semigroup,~neutral :~'a{\char125};\\ \hspace*{0pt}fun semigroup{\char95}monoid (A{\char95}:'a monoid) = {\char35}Program{\char95}{\char95}semigroup{\char95}monoid A{\char95};\\ \hspace*{0pt}fun neutral (A{\char95}:'a monoid) = {\char35}neutral A{\char95};\\ \hspace*{0pt}\\ @@ -356,7 +356,7 @@ \hspace*{0pt}fun plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n)\\ \hspace*{0pt} ~| plus{\char95}nat Zero{\char95}nat n = n;\\ \hspace*{0pt}\\ -\hspace*{0pt}val neutral{\char95}nat :~nat = Suc Zero{\char95}nat;\\ +\hspace*{0pt}val neutral{\char95}nat :~nat = Suc Zero{\char95}nat\\ \hspace*{0pt}\\ \hspace*{0pt}fun mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat\\ \hspace*{0pt} ~| mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\ @@ -364,12 +364,12 @@ \hspace*{0pt}val semigroup{\char95}nat = {\char123}mult = mult{\char95}nat{\char125}~:~nat semigroup;\\ \hspace*{0pt}\\ \hspace*{0pt}val monoid{\char95}nat =\\ -\hspace*{0pt} ~{\char123}Program{\char95}{\char95}semigroup{\char95}monoid = semigroup{\char95}nat, neutral = neutral{\char95}nat{\char125}~:\\ +\hspace*{0pt} ~{\char123}Program{\char95}{\char95}semigroup{\char95}monoid = semigroup{\char95}nat,~neutral = neutral{\char95}nat{\char125}~:\\ \hspace*{0pt} ~nat monoid;\\ \hspace*{0pt}\\ \hspace*{0pt}fun bexp n = pow monoid{\char95}nat n (Suc (Suc Zero{\char95}nat));\\ \hspace*{0pt}\\ -\hspace*{0pt}end; (*struct Example*)% +\hspace*{0pt}end;~(*struct Example*)% \end{isamarkuptext}% \isamarkuptrue% % @@ -675,7 +675,7 @@ \hspace*{0pt} ~| plus{\char95}nat m Zero{\char95}nat = m\\ \hspace*{0pt} ~| plus{\char95}nat Zero{\char95}nat n = n;\\ \hspace*{0pt}\\ -\hspace*{0pt}end; (*struct Example*)% +\hspace*{0pt}end;~(*struct Example*)% \end{isamarkuptext}% \isamarkuptrue% % @@ -794,7 +794,7 @@ \hspace*{0pt} ~~~~~~~~~~~~else collect{\char95}duplicates A{\char95}~xs (z ::~ys) zs)\\ \hspace*{0pt} ~~~~~else collect{\char95}duplicates A{\char95}~(z ::~xs) (z ::~ys) zs);\\ \hspace*{0pt}\\ -\hspace*{0pt}end; (*struct Example*)% +\hspace*{0pt}end;~(*struct Example*)% \end{isamarkuptext}% \isamarkuptrue% % @@ -918,7 +918,7 @@ \hspace*{0pt}type 'a eq = {\char123}eq :~'a -> 'a -> bool{\char125};\\ \hspace*{0pt}fun eq (A{\char95}:'a eq) = {\char35}eq A{\char95};\\ \hspace*{0pt}\\ -\hspace*{0pt}type 'a ord = {\char123}less{\char95}eq :~'a -> 'a -> bool, less :~'a -> 'a -> bool{\char125};\\ +\hspace*{0pt}type 'a ord = {\char123}less{\char95}eq :~'a -> 'a -> bool,~less :~'a -> 'a -> bool{\char125};\\ \hspace*{0pt}fun less{\char95}eq (A{\char95}:'a ord) = {\char35}less{\char95}eq A{\char95};\\ \hspace*{0pt}fun less (A{\char95}:'a ord) = {\char35}less A{\char95};\\ \hspace*{0pt}\\ @@ -930,16 +930,16 @@ \hspace*{0pt}type 'a order = {\char123}Orderings{\char95}{\char95}preorder{\char95}order :~'a preorder{\char125};\\ \hspace*{0pt}fun preorder{\char95}order (A{\char95}:'a order) = {\char35}Orderings{\char95}{\char95}preorder{\char95}order A{\char95};\\ \hspace*{0pt}\\ -\hspace*{0pt}fun less{\char95}eqa (A1{\char95}, A2{\char95}) B{\char95}~(x1, y1) (x2, y2) =\\ +\hspace*{0pt}fun less{\char95}eqa (A1{\char95},~A2{\char95}) B{\char95}~(x1,~y1) (x2,~y2) =\\ \hspace*{0pt} ~less ((ord{\char95}preorder o preorder{\char95}order) A2{\char95}) x1 x2 orelse\\ \hspace*{0pt} ~~~eqop A1{\char95}~x1 x2 andalso\\ \hspace*{0pt} ~~~~~less{\char95}eq ((ord{\char95}preorder o preorder{\char95}order) B{\char95}) y1 y2\\ -\hspace*{0pt} ~| less{\char95}eqa (A1{\char95}, A2{\char95}) B{\char95}~(x1, y1) (x2, y2) =\\ +\hspace*{0pt} ~| less{\char95}eqa (A1{\char95},~A2{\char95}) B{\char95}~(x1,~y1) (x2,~y2) =\\ \hspace*{0pt} ~~~less ((ord{\char95}preorder o preorder{\char95}order) A2{\char95}) x1 x2 orelse\\ \hspace*{0pt} ~~~~~eqop A1{\char95}~x1 x2 andalso\\ \hspace*{0pt} ~~~~~~~less{\char95}eq ((ord{\char95}preorder o preorder{\char95}order) B{\char95}) y1 y2;\\ \hspace*{0pt}\\ -\hspace*{0pt}end; (*struct Example*)% +\hspace*{0pt}end;~(*struct Example*)% \end{isamarkuptext}% \isamarkuptrue% % @@ -1052,10 +1052,10 @@ \hspace*{0pt} ~| list{\char95}all2 p xs [] = null xs\\ \hspace*{0pt} ~| list{\char95}all2 p [] ys = null ys;\\ \hspace*{0pt}\\ -\hspace*{0pt}fun eq{\char95}monotype (Mono (tyco1, typargs1)) (Mono (tyco2, typargs2)) =\\ +\hspace*{0pt}fun eq{\char95}monotype (Mono (tyco1,~typargs1)) (Mono (tyco2,~typargs2)) =\\ \hspace*{0pt} ~eq{\char95}nat tyco1 tyco2 andalso list{\char95}all2 eq{\char95}monotype typargs1 typargs2;\\ \hspace*{0pt}\\ -\hspace*{0pt}end; (*struct Example*)% +\hspace*{0pt}end;~(*struct Example*)% \end{isamarkuptext}% \isamarkuptrue% % @@ -1108,12 +1108,12 @@ \begin{isamarkuptext}% \isatypewriter% \noindent% -\hspace*{0pt}strict{\char95}dequeue ::~forall a. Queue a -> (a, Queue a);\\ -\hspace*{0pt}strict{\char95}dequeue (Queue xs (y :~ys)) = (y, Queue xs ys);\\ +\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\ +\hspace*{0pt}strict{\char95}dequeue (Queue xs (y :~ys)) = (y,~Queue xs ys);\\ \hspace*{0pt}strict{\char95}dequeue (Queue xs []) =\\ \hspace*{0pt} ~let {\char123}\\ \hspace*{0pt} ~~~(y :~ys) = rev xs;\\ -\hspace*{0pt} ~{\char125}~in (y, Queue [] ys);% +\hspace*{0pt} ~{\char125}~in (y,~Queue [] ys);% \end{isamarkuptext}% \isamarkuptrue% % @@ -1204,13 +1204,13 @@ \begin{isamarkuptext}% \isatypewriter% \noindent% -\hspace*{0pt}empty{\char95}queue ::~forall a. a;\\ +\hspace*{0pt}empty{\char95}queue ::~forall a.~a;\\ \hspace*{0pt}empty{\char95}queue = error {\char34}empty{\char95}queue{\char34};\\ \hspace*{0pt}\\ -\hspace*{0pt}strict{\char95}dequeue' ::~forall a. Queue a -> (a, Queue a);\\ +\hspace*{0pt}strict{\char95}dequeue' ::~forall a.~Queue a -> (a,~Queue a);\\ \hspace*{0pt}strict{\char95}dequeue' (Queue xs []) =\\ \hspace*{0pt} ~(if nulla xs then empty{\char95}queue else strict{\char95}dequeue' (Queue [] (rev xs)));\\ -\hspace*{0pt}strict{\char95}dequeue' (Queue xs (y :~ys)) = (y, Queue xs ys);% +\hspace*{0pt}strict{\char95}dequeue' (Queue xs (y :~ys)) = (y,~Queue xs ys);% \end{isamarkuptext}% \isamarkuptrue% % diff -r 96cf8edb6249 -r 62e0f892e525 doc-src/IsarAdvanced/Codegen/Thy/examples/Example.hs --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/Example.hs Thu Jan 01 21:28:38 2009 +0100 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/Example.hs Thu Jan 01 21:30:13 2009 +0100 @@ -1,3 +1,5 @@ +{-# OPTIONS_GHC -fglasgow-exts #-} + module Example where { diff -r 96cf8edb6249 -r 62e0f892e525 doc-src/IsarAdvanced/Codegen/Thy/examples/example.ML --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/example.ML Thu Jan 01 21:28:38 2009 +0100 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/example.ML Thu Jan 01 21:30:13 2009 +0100 @@ -11,7 +11,7 @@ datatype 'a queue = Queue of 'a list * 'a list; -val empty : 'a queue = Queue ([], []); +val empty : 'a queue = Queue ([], []) fun dequeue (Queue ([], [])) = (NONE, Queue ([], [])) | dequeue (Queue (xs, y :: ys)) = (SOME y, Queue (xs, ys)) diff -r 96cf8edb6249 -r 62e0f892e525 doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex --- a/doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex Thu Jan 01 21:28:38 2009 +0100 +++ b/doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex Thu Jan 01 21:30:13 2009 +0100 @@ -440,7 +440,7 @@ \isamarkuptrue% % \begin{isamarkuptext}% -The the key to this error message is the matrix at the bottom. The rows +The key to this error message is the matrix at the bottom. The rows of that matrix correspond to the different recursive calls (In our case, there is just one). The columns are the function's arguments (expressed through different measure functions, which map the @@ -674,7 +674,7 @@ {\isacharbar}\ {\isachardoublequoteopen}And\ X\ X\ {\isacharequal}\ X{\isachardoublequoteclose}% \begin{isamarkuptext}% This definition is useful, because the equations can directly be used - as simplification rules rules. But the patterns overlap: For example, + as simplification rules. But the patterns overlap: For example, the expression \isa{And\ T\ T} is matched by both the first and the second equation. By default, Isabelle makes the patterns disjoint by splitting them up, producing instances:% @@ -829,13 +829,21 @@ either \isa{{\isadigit{0}}}, \isa{{\isadigit{1}}} or \isa{n\ {\isacharplus}\ {\isadigit{2}}}: \begin{isabelle}% -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}P\ x{\isachardot}\ {\isasymlbrakk}x\ {\isacharequal}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ P{\isacharsemicolon}\ x\ {\isacharequal}\ {\isadigit{1}}\ {\isasymLongrightarrow}\ P{\isacharsemicolon}\ {\isasymAnd}n{\isachardot}\ x\ {\isacharequal}\ n\ {\isacharplus}\ {\isadigit{2}}\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}P\ x{\isachardot}\ {\isasymlbrakk}x\ {\isacharequal}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ P{\isacharsemicolon}\ x\ {\isacharequal}\ {\isadigit{1}}\ {\isasymLongrightarrow}\ P{\isacharsemicolon}\ {\isasymAnd}n{\isachardot}\ x\ {\isacharequal}\ n\ {\isacharplus}\ {\isadigit{2}}\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\isanewline +\ {\isadigit{2}}{\isachardot}\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ {\isadigit{1}}\ {\isacharequal}\ {\isadigit{1}}\isanewline +\ {\isadigit{3}}{\isachardot}\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isadigit{1}}\ {\isacharequal}\ {\isadigit{1}}\isanewline +\ {\isadigit{4}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isadigit{0}}\ {\isacharequal}\ n\ {\isacharplus}\ {\isadigit{2}}\ {\isasymLongrightarrow}\ {\isadigit{1}}\ {\isacharequal}\ fib{\isadigit{2}}{\isacharunderscore}sumC\ n\ {\isacharplus}\ fib{\isadigit{2}}{\isacharunderscore}sumC\ {\isacharparenleft}Suc\ n{\isacharparenright}\isanewline +\ {\isadigit{5}}{\isachardot}\ {\isadigit{1}}\ {\isacharequal}\ {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isadigit{1}}\ {\isacharequal}\ {\isadigit{1}}\isanewline +\ {\isadigit{6}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isadigit{1}}\ {\isacharequal}\ n\ {\isacharplus}\ {\isadigit{2}}\ {\isasymLongrightarrow}\ {\isadigit{1}}\ {\isacharequal}\ fib{\isadigit{2}}{\isacharunderscore}sumC\ n\ {\isacharplus}\ fib{\isadigit{2}}{\isacharunderscore}sumC\ {\isacharparenleft}Suc\ n{\isacharparenright}\isanewline +\ {\isadigit{7}}{\isachardot}\ {\isasymAnd}n\ na{\isachardot}\isanewline +\isaindent{\ {\isadigit{7}}{\isachardot}\ \ \ \ }n\ {\isacharplus}\ {\isadigit{2}}\ {\isacharequal}\ na\ {\isacharplus}\ {\isadigit{2}}\ {\isasymLongrightarrow}\isanewline +\isaindent{\ {\isadigit{7}}{\isachardot}\ \ \ \ }fib{\isadigit{2}}{\isacharunderscore}sumC\ n\ {\isacharplus}\ fib{\isadigit{2}}{\isacharunderscore}sumC\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ fib{\isadigit{2}}{\isacharunderscore}sumC\ na\ {\isacharplus}\ fib{\isadigit{2}}{\isacharunderscore}sumC\ {\isacharparenleft}Suc\ na{\isacharparenright}% \end{isabelle} This is an arithmetic triviality, but unfortunately the \isa{arith} method cannot handle this specific form of an elimination rule. However, we can use the method \isa{atomize{\isacharunderscore}elim} to do an ad-hoc conversion to a disjunction of - existentials, which can then be soved by the arithmetic decision procedure. + existentials, which can then be solved by the arithmetic decision procedure. Pattern compatibility and termination are automatic as usual.% \end{isamarkuptxt}% \isamarkuptrue% diff -r 96cf8edb6249 -r 62e0f892e525 doc-src/LaTeXsugar/Sugar/document/Sugar.tex --- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Thu Jan 01 21:28:38 2009 +0100 +++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Thu Jan 01 21:30:13 2009 +0100 @@ -148,7 +148,7 @@ \begin{isamarkuptext}% If you print anything, especially theorems, containing schematic variables they are prefixed with a question mark: -\verb!@!\verb!{thm conjI}! results in \isa{{\isasymlbrakk}{\isacharquery}P{\isacharsemicolon}\ {\isacharquery}Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}P\ {\isasymand}\ {\isacharquery}Q}. Most of the time +\verb!@!\verb!{thm conjI}! results in \isa{{\isasymlbrakk}P{\isacharsemicolon}\ Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isasymand}\ Q}. Most of the time you would rather not see the question marks. There is an attribute \verb!no_vars! that you can attach to the theorem that turns its schematic into ordinary free variables: \verb!@!\verb!{thm conjI[no_vars]}! diff -r 96cf8edb6249 -r 62e0f892e525 doc-src/Locales/Locales/document/Examples.tex --- a/doc-src/Locales/Locales/document/Examples.tex Thu Jan 01 21:28:38 2009 +0100 +++ b/doc-src/Locales/Locales/document/Examples.tex Thu Jan 01 21:30:13 2009 +0100 @@ -1222,7 +1222,7 @@ \endisadelimvisible % \isatagvisible -\isacommand{interpretation}\isamarkupfalse% +\isacommand{sublocale}\isamarkupfalse% \ total{\isacharunderscore}order\ {\isasymsubseteq}\ lattice% \begin{isamarkuptxt}% This enters the context of locale \isa{total{\isacharunderscore}order}, in @@ -1325,7 +1325,7 @@ Similarly, total orders are distributive lattices.% \end{isamarkuptext}% \isamarkuptrue% -\ \ \isacommand{interpretation}\isamarkupfalse% +\ \ \isacommand{sublocale}\isamarkupfalse% \ total{\isacharunderscore}order\ {\isasymsubseteq}\ distrib{\isacharunderscore}lattice\isanewline % \isadelimproof diff -r 96cf8edb6249 -r 62e0f892e525 doc-src/Locales/Locales/document/Examples1.tex --- a/doc-src/Locales/Locales/document/Examples1.tex Thu Jan 01 21:28:38 2009 +0100 +++ b/doc-src/Locales/Locales/document/Examples1.tex Thu Jan 01 21:30:13 2009 +0100 @@ -74,7 +74,7 @@ % \isatagvisible \isacommand{interpretation}\isamarkupfalse% -\ nat{\isacharcolon}\ partial{\isacharunderscore}order\ {\isacharbrackleft}{\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}{\isacharbrackright}% +\ nat{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}% \begin{isamarkuptxt}% The locale name is succeeded by a \emph{parameter instantiation}. In general, this is a list of terms, which refer to diff -r 96cf8edb6249 -r 62e0f892e525 doc-src/Locales/Locales/document/Examples2.tex --- a/doc-src/Locales/Locales/document/Examples2.tex Thu Jan 01 21:28:38 2009 +0100 +++ b/doc-src/Locales/Locales/document/Examples2.tex Thu Jan 01 21:30:13 2009 +0100 @@ -34,7 +34,7 @@ % \isatagvisible \isacommand{interpretation}\isamarkupfalse% -\ nat{\isacharcolon}\ partial{\isacharunderscore}order\ {\isacharbrackleft}{\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ {\isacharbrackleft}nat{\isacharcomma}\ nat{\isacharbrackright}\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}{\isacharbrackright}\isanewline +\ nat{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ {\isacharbrackleft}nat{\isacharcomma}\ nat{\isacharbrackright}\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline \ \ \isakeyword{where}\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline \isacommand{proof}\isamarkupfalse% \ {\isacharminus}% diff -r 96cf8edb6249 -r 62e0f892e525 doc-src/Locales/Locales/document/Examples3.tex --- a/doc-src/Locales/Locales/document/Examples3.tex Thu Jan 01 21:28:38 2009 +0100 +++ b/doc-src/Locales/Locales/document/Examples3.tex Thu Jan 01 21:30:13 2009 +0100 @@ -43,7 +43,7 @@ % \isatagvisible \isacommand{interpretation}\isamarkupfalse% -\ nat{\isacharcolon}\ partial{\isacharunderscore}order\ {\isacharbrackleft}{\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}{\isacharbrackright}\isanewline +\ nat{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline \ \ \isakeyword{where}\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ {\isacharparenleft}op\ {\isasymle}{\isacharparenright}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline \isacommand{proof}\isamarkupfalse% \ {\isacharminus}\isanewline @@ -53,7 +53,7 @@ \ unfold{\isacharunderscore}locales\ auto\isanewline \ \ \isacommand{then}\isamarkupfalse% \ \isacommand{interpret}\isamarkupfalse% -\ nat{\isacharcolon}\ partial{\isacharunderscore}order\ {\isacharbrackleft}{\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ {\isacharbrackleft}nat{\isacharcomma}\ nat{\isacharbrackright}\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}{\isacharbrackright}\ \isacommand{{\isachardot}}\isamarkupfalse% +\ nat{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ {\isacharbrackleft}nat{\isacharcomma}\ nat{\isacharbrackright}\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse% \isanewline \ \ \isacommand{show}\isamarkupfalse% \ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ {\isacharparenleft}op\ {\isasymle}{\isacharparenright}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline @@ -91,8 +91,8 @@ \begin{isamarkuptext}% Further interpretations are necessary to reuse theorems from the other locales. In \isa{lattice} the operations \isa{{\isasymsqinter}} and - \isa{{\isasymsqunion}} are substituted by \isa{ord{\isacharunderscore}class{\isachardot}min} and - \isa{ord{\isacharunderscore}class{\isachardot}max}. The entire proof for the + \isa{{\isasymsqunion}} are substituted by \isa{min} and + \isa{max}. The entire proof for the interpretation is reproduced in order to give an example of a more elaborate interpretation proof.% \end{isamarkuptext}% @@ -104,7 +104,7 @@ % \isatagvisible \isacommand{interpretation}\isamarkupfalse% -\ nat{\isacharcolon}\ lattice\ {\isacharbrackleft}{\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}{\isacharbrackright}\isanewline +\ nat{\isacharcolon}\ lattice\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline \ \ \isakeyword{where}\ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ min\ x\ y{\isachardoublequoteclose}\isanewline \ \ \ \ \isakeyword{and}\ {\isachardoublequoteopen}lattice{\isachardot}join\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ max\ x\ y{\isachardoublequoteclose}\isanewline \isacommand{proof}\isamarkupfalse% @@ -143,7 +143,7 @@ \isamarkuptrue% \ \ \isacommand{then}\isamarkupfalse% \ \isacommand{interpret}\isamarkupfalse% -\ nat{\isacharcolon}\ lattice\ {\isacharbrackleft}{\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}{\isacharbrackright}\ \isacommand{{\isachardot}}\isamarkupfalse% +\ nat{\isacharcolon}\ lattice\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse% \isanewline \ \ \isacommand{show}\isamarkupfalse% \ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ min\ x\ y{\isachardoublequoteclose}\isanewline @@ -174,7 +174,7 @@ % \isatagvisible \isacommand{interpretation}\isamarkupfalse% -\ nat{\isacharcolon}\ total{\isacharunderscore}order\ {\isacharbrackleft}{\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}{\isacharbrackright}\isanewline +\ nat{\isacharcolon}\ total{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline \ \ \isacommand{by}\isamarkupfalse% \ unfold{\isacharunderscore}locales\ arith% \endisatagvisible @@ -196,11 +196,11 @@ \isa{nat{\isachardot}less{\isacharunderscore}def} from locale \isa{partial{\isacharunderscore}order}: \\ \quad \isa{{\isacharparenleft}{\isacharquery}x\ {\isacharless}\ {\isacharquery}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isacharquery}x\ {\isasymle}\ {\isacharquery}y\ {\isasymand}\ {\isacharquery}x\ {\isasymnoteq}\ {\isacharquery}y{\isacharparenright}} \\ \isa{nat{\isachardot}meet{\isacharunderscore}left} from locale \isa{lattice}: \\ - \quad \isa{ord{\isacharunderscore}class{\isachardot}min\ {\isacharquery}x\ {\isacharquery}y\ {\isasymle}\ {\isacharquery}x} \\ + \quad \isa{min\ {\isacharquery}x\ {\isacharquery}y\ {\isasymle}\ {\isacharquery}x} \\ \isa{nat{\isachardot}join{\isacharunderscore}distr} from locale \isa{distrib{\isacharunderscore}lattice}: \\ - \quad \isa{ord{\isacharunderscore}class{\isachardot}max\ {\isacharquery}x\ {\isacharparenleft}ord{\isacharunderscore}class{\isachardot}min\ {\isacharquery}y\ {\isacharquery}z{\isacharparenright}\ {\isacharequal}\ ord{\isacharunderscore}class{\isachardot}min\ {\isacharparenleft}ord{\isacharunderscore}class{\isachardot}max\ {\isacharquery}x\ {\isacharquery}y{\isacharparenright}\ {\isacharparenleft}ord{\isacharunderscore}class{\isachardot}max\ {\isacharquery}x\ {\isacharquery}z{\isacharparenright}} \\ + \quad \isa{lattice{\isachardot}join\ op\ {\isasymle}\ {\isacharquery}x\ {\isacharparenleft}lattice{\isachardot}meet\ op\ {\isasymle}\ {\isacharquery}y\ {\isacharquery}z{\isacharparenright}\ {\isacharequal}\ lattice{\isachardot}meet\ op\ {\isasymle}\ {\isacharparenleft}lattice{\isachardot}join\ op\ {\isasymle}\ {\isacharquery}x\ {\isacharquery}y{\isacharparenright}\ {\isacharparenleft}lattice{\isachardot}join\ op\ {\isasymle}\ {\isacharquery}x\ {\isacharquery}z{\isacharparenright}} \\ \isa{nat{\isachardot}less{\isacharunderscore}total} from locale \isa{total{\isacharunderscore}order}: \\ - \quad \isa{{\isacharquery}x\ {\isacharless}\ {\isacharquery}y\ {\isasymor}\ {\isacharquery}x\ {\isacharequal}\ {\isacharquery}y\ {\isasymor}\ {\isacharquery}y\ {\isacharless}\ {\isacharquery}x} + \quad \isa{partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharquery}x\ {\isacharquery}y\ {\isasymor}\ {\isacharquery}x\ {\isacharequal}\ {\isacharquery}y\ {\isasymor}\ partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharquery}y\ {\isacharquery}x} \end{tabular} \end{center} \hrule @@ -244,7 +244,7 @@ \end{isamarkuptext}% \isamarkuptrue% \isacommand{interpretation}\isamarkupfalse% -\ nat{\isacharunderscore}dvd{\isacharcolon}\ partial{\isacharunderscore}order\ {\isacharbrackleft}{\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}{\isacharbrackright}\isanewline +\ nat{\isacharunderscore}dvd{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline \ \ \isakeyword{where}\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ dvd\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ dvd\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline % \isadelimproof @@ -260,7 +260,7 @@ \ unfold{\isacharunderscore}locales\ {\isacharparenleft}auto\ simp{\isacharcolon}\ dvd{\isacharunderscore}def{\isacharparenright}\isanewline \ \ \isacommand{then}\isamarkupfalse% \ \isacommand{interpret}\isamarkupfalse% -\ nat{\isacharunderscore}dvd{\isacharcolon}\ partial{\isacharunderscore}order\ {\isacharbrackleft}{\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}{\isacharbrackright}\ \isacommand{{\isachardot}}\isamarkupfalse% +\ nat{\isacharunderscore}dvd{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse% \isanewline \ \ \isacommand{show}\isamarkupfalse% \ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ dvd\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ dvd\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline @@ -285,7 +285,7 @@ \end{isamarkuptext}% \isamarkuptrue% \isacommand{interpretation}\isamarkupfalse% -\ nat{\isacharunderscore}dvd{\isacharcolon}\ lattice\ {\isacharbrackleft}{\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}{\isacharbrackright}\isanewline +\ nat{\isacharunderscore}dvd{\isacharcolon}\ lattice\ {\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline \ \ \isakeyword{where}\ nat{\isacharunderscore}dvd{\isacharunderscore}meet{\isacharunderscore}eq{\isacharcolon}\isanewline \ \ \ \ \ \ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ dvd\ {\isacharequal}\ gcd{\isachardoublequoteclose}\isanewline \ \ \ \ \isakeyword{and}\ nat{\isacharunderscore}dvd{\isacharunderscore}join{\isacharunderscore}eq{\isacharcolon}\isanewline @@ -316,7 +316,7 @@ \isanewline \ \ \isacommand{then}\isamarkupfalse% \ \isacommand{interpret}\isamarkupfalse% -\ nat{\isacharunderscore}dvd{\isacharcolon}\ lattice\ {\isacharbrackleft}{\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}{\isacharbrackright}\ \isacommand{{\isachardot}}\isamarkupfalse% +\ nat{\isacharunderscore}dvd{\isacharcolon}\ lattice\ {\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse% \isanewline \ \ \isacommand{show}\isamarkupfalse% \ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ dvd\ {\isacharequal}\ gcd{\isachardoublequoteclose}\isanewline @@ -390,7 +390,7 @@ \isatagvisible \isacommand{interpretation}\isamarkupfalse% \ nat{\isacharunderscore}dvd{\isacharcolon}\isanewline -\ \ distrib{\isacharunderscore}lattice\ {\isacharbrackleft}{\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}{\isacharbrackright}\isanewline +\ \ distrib{\isacharunderscore}lattice\ {\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline \ \ \isacommand{apply}\isamarkupfalse% \ unfold{\isacharunderscore}locales% \begin{isamarkuptxt}% @@ -434,7 +434,7 @@ \isa{nat{\isacharunderscore}dvd{\isachardot}meet{\isacharunderscore}left} from locale \isa{lattice}: \\ \quad \isa{gcd\ {\isacharquery}x\ {\isacharquery}y\ dvd\ {\isacharquery}x} \\ \isa{nat{\isacharunderscore}dvd{\isachardot}join{\isacharunderscore}distr} from locale \isa{distrib{\isacharunderscore}lattice}: \\ - \quad \isa{lcm\ {\isacharquery}x\ {\isacharparenleft}gcd\ {\isacharquery}y\ {\isacharquery}z{\isacharparenright}\ {\isacharequal}\ gcd\ {\isacharparenleft}lcm\ {\isacharquery}x\ {\isacharquery}y{\isacharparenright}\ {\isacharparenleft}lcm\ {\isacharquery}x\ {\isacharquery}z{\isacharparenright}} \\ + \quad \isa{lattice{\isachardot}join\ op\ dvd\ {\isacharquery}x\ {\isacharparenleft}lattice{\isachardot}meet\ op\ dvd\ {\isacharquery}y\ {\isacharquery}z{\isacharparenright}\ {\isacharequal}\ lattice{\isachardot}meet\ op\ dvd\ {\isacharparenleft}lattice{\isachardot}join\ op\ dvd\ {\isacharquery}x\ {\isacharquery}y{\isacharparenright}\ {\isacharparenleft}lattice{\isachardot}join\ op\ dvd\ {\isacharquery}x\ {\isacharquery}z{\isacharparenright}} \\ \end{tabular} \end{center} \hrule @@ -476,7 +476,7 @@ \isamarkuptrue% \ \ \isacommand{locale}\isamarkupfalse% \ order{\isacharunderscore}preserving\ {\isacharequal}\isanewline -\ \ \ \ partial{\isacharunderscore}order\ {\isacharplus}\ partial{\isacharunderscore}order\ le{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasympreceq}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ {\isacharplus}\isanewline +\ \ \ \ partial{\isacharunderscore}order\ {\isacharplus}\ po{\isacharprime}{\isacharcolon}\ partial{\isacharunderscore}order\ le{\isacharprime}\ \isakeyword{for}\ le{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasympreceq}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ {\isacharplus}\isanewline \ \ \ \ \isakeyword{fixes}\ {\isasymphi}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isachardoublequoteclose}\isanewline \ \ \ \ \isakeyword{assumes}\ hom{\isacharunderscore}le{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymsqsubseteq}\ y\ {\isasymLongrightarrow}\ {\isasymphi}\ x\ {\isasympreceq}\ {\isasymphi}\ y{\isachardoublequoteclose}% \begin{isamarkuptext}% @@ -505,7 +505,8 @@ \isamarkuptrue% % \begin{isamarkuptext}% -The locale \isa{order{\isacharunderscore}preserving} contains theorems for both +% FIXME needs update + The locale \isa{order{\isacharunderscore}preserving} contains theorems for both orders \isa{{\isasymsqsubseteq}} and \isa{{\isasympreceq}}. How can one refer to a theorem for a particular order, \isa{{\isasymsqsubseteq}} or \isa{{\isasympreceq}}? Names in locales are qualified by the locale parameters. More precisely, a name is @@ -529,16 +530,17 @@ \endisadeliminvisible % \begin{isamarkuptext}% -\isa{le{\isachardot}less{\isacharunderscore}le{\isacharunderscore}trans}: \isa{{\isasymlbrakk}{\isacharquery}x\ {\isasymsqsubset}\ {\isacharquery}y{\isacharsemicolon}\ {\isacharquery}y\ {\isasymsqsubseteq}\ {\isacharquery}z{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}x\ {\isasymsqsubset}\ {\isacharquery}z} +% FIXME needs update? + \isa{less{\isacharunderscore}le{\isacharunderscore}trans}: \isa{{\isasymlbrakk}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasympreceq}\ {\isacharquery}x\ {\isacharquery}y{\isacharsemicolon}\ {\isacharquery}y\ {\isasympreceq}\ {\isacharquery}z{\isasymrbrakk}\ {\isasymLongrightarrow}\ partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasympreceq}\ {\isacharquery}x\ {\isacharquery}z} - \isa{le{\isacharunderscore}le{\isacharprime}{\isacharunderscore}{\isasymphi}{\isachardot}hom{\isacharunderscore}le}: \isa{{\isacharquery}x\ {\isasymsqsubseteq}\ {\isacharquery}y\ {\isasymLongrightarrow}\ {\isasymphi}\ {\isacharquery}x\ {\isasympreceq}\ {\isasymphi}\ {\isacharquery}y}% + \isa{hom{\isacharunderscore}le}: \isa{{\isacharquery}x\ {\isasymsqsubseteq}\ {\isacharquery}y\ {\isasymLongrightarrow}\ {\isasymphi}\ {\isacharquery}x\ {\isasympreceq}\ {\isasymphi}\ {\isacharquery}y}% \end{isamarkuptext}% \isamarkuptrue% % \begin{isamarkuptext}% When renaming a locale, the morphism is also applied to the qualifiers. Hence theorems for the partial order \isa{{\isasympreceq}} - are qualified by \isa{le{\isacharprime}}. For example, \isa{le{\isacharprime}{\isachardot}less{\isacharunderscore}le{\isacharunderscore}trans}: \begin{isabelle}% + are qualified by \isa{le{\isacharprime}}. For example, \isa{po{\isacharprime}{\isachardot}less{\isacharunderscore}le{\isacharunderscore}trans}: \begin{isabelle}% \ \ {\isasymlbrakk}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasympreceq}\ {\isacharquery}x\ {\isacharquery}y{\isacharsemicolon}\ {\isacharquery}y\ {\isasympreceq}\ {\isacharquery}z{\isasymrbrakk}\isanewline \isaindent{\ \ }{\isasymLongrightarrow}\ partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasympreceq}\ {\isacharquery}x\ {\isacharquery}z% \end{isabelle}% @@ -560,7 +562,8 @@ \endisadeliminvisible % \begin{isamarkuptext}% -This example reveals that there is no infix syntax for the strict +% FIXME needs update? + This example reveals that there is no infix syntax for the strict version of \isa{{\isasympreceq}}! This can, of course, not be introduced automatically, but it can be declared manually through an abbreviation.% \end{isamarkuptext}% @@ -589,7 +592,7 @@ \end{isamarkuptext}% \isamarkuptrue% \ \ \isacommand{locale}\isamarkupfalse% -\ lattice{\isacharunderscore}hom\ {\isacharequal}\ lattice\ {\isacharplus}\ lattice\ le{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasympreceq}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ {\isacharplus}\isanewline +\ lattice{\isacharunderscore}hom\ {\isacharequal}\ lattice\ {\isacharplus}\ lat{\isacharprime}{\isacharbang}{\isacharcolon}\ lattice\ le{\isacharprime}\ \isakeyword{for}\ le{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasympreceq}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ {\isacharplus}\isanewline \ \ \ \ \isakeyword{fixes}\ {\isasymphi}\isanewline \ \ \ \ \isakeyword{assumes}\ hom{\isacharunderscore}meet{\isacharcolon}\isanewline \ \ \ \ \ \ \ \ {\isachardoublequoteopen}{\isasymphi}\ {\isacharparenleft}lattice{\isachardot}meet\ le\ x\ y{\isacharparenright}\ {\isacharequal}\ lattice{\isachardot}meet\ le{\isacharprime}\ {\isacharparenleft}{\isasymphi}\ x{\isacharparenright}\ {\isacharparenleft}{\isasymphi}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline @@ -598,17 +601,17 @@ \isanewline \ \ \isacommand{abbreviation}\isamarkupfalse% \ {\isacharparenleft}\isakeyword{in}\ lattice{\isacharunderscore}hom{\isacharparenright}\isanewline -\ \ \ \ meet{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymsqinter}{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{where}\ {\isachardoublequoteopen}meet{\isacharprime}\ {\isasymequiv}\ le{\isacharprime}{\isachardot}meet{\isachardoublequoteclose}\isanewline +\ \ \ \ meet{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymsqinter}{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{where}\ {\isachardoublequoteopen}meet{\isacharprime}\ {\isasymequiv}\ lat{\isacharprime}{\isachardot}meet{\isachardoublequoteclose}\isanewline \ \ \isacommand{abbreviation}\isamarkupfalse% \ {\isacharparenleft}\isakeyword{in}\ lattice{\isacharunderscore}hom{\isacharparenright}\isanewline -\ \ \ \ join{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymsqunion}{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{where}\ {\isachardoublequoteopen}join{\isacharprime}\ {\isasymequiv}\ le{\isacharprime}{\isachardot}join{\isachardoublequoteclose}% +\ \ \ \ join{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymsqunion}{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{where}\ {\isachardoublequoteopen}join{\isacharprime}\ {\isasymequiv}\ lat{\isacharprime}{\isachardot}join{\isachardoublequoteclose}% \begin{isamarkuptext}% A homomorphism is an endomorphism if both orders coincide.% \end{isamarkuptext}% \isamarkuptrue% \ \ \isacommand{locale}\isamarkupfalse% \ lattice{\isacharunderscore}end\ {\isacharequal}\isanewline -\ \ \ \ lattice{\isacharunderscore}hom\ le\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymsqsubseteq}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ le\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymsqsubseteq}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}% +\ \ \ \ lattice{\isacharunderscore}hom\ le\ le\ \isakeyword{for}\ le\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymsqsubseteq}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}% \begin{isamarkuptext}% The inheritance diagram of the situation we have now is shown in Figure~\ref{fig:hom}, where the dashed line depicts an @@ -659,7 +662,7 @@ interpretation is used to assert this.% \end{isamarkuptext}% \isamarkuptrue% -\ \ \isacommand{interpretation}\isamarkupfalse% +\ \ \isacommand{sublocale}\isamarkupfalse% \ lattice{\isacharunderscore}hom\ {\isasymsubseteq}\ order{\isacharunderscore}preserving% \isadelimproof \ % @@ -675,7 +678,7 @@ \ \ \ \ \isacommand{then}\isamarkupfalse% \ \isacommand{have}\isamarkupfalse% \ {\isachardoublequoteopen}y\ {\isacharequal}\ {\isacharparenleft}x\ {\isasymsqunion}\ y{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% -\ {\isacharparenleft}simp\ add{\isacharcolon}\ le{\isachardot}join{\isacharunderscore}connection{\isacharparenright}\isanewline +\ {\isacharparenleft}simp\ add{\isacharcolon}\ join{\isacharunderscore}connection{\isacharparenright}\isanewline \ \ \ \ \isacommand{then}\isamarkupfalse% \ \isacommand{have}\isamarkupfalse% \ {\isachardoublequoteopen}{\isasymphi}\ y\ {\isacharequal}\ {\isacharparenleft}{\isasymphi}\ x\ {\isasymsqunion}{\isacharprime}\ {\isasymphi}\ y{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% @@ -683,7 +686,7 @@ \ \ \ \ \isacommand{then}\isamarkupfalse% \ \isacommand{show}\isamarkupfalse% \ {\isachardoublequoteopen}{\isasymphi}\ x\ {\isasympreceq}\ {\isasymphi}\ y{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% -\ {\isacharparenleft}simp\ add{\isacharcolon}\ le{\isacharprime}{\isachardot}join{\isacharunderscore}connection{\isacharparenright}\isanewline +\ {\isacharparenleft}simp\ add{\isacharcolon}\ lat{\isacharprime}{\isachardot}join{\isacharunderscore}connection{\isacharparenright}\isanewline \ \ \isacommand{qed}\isamarkupfalse% % \endisatagproof @@ -697,7 +700,7 @@ Theorems and other declarations --- syntax, in particular --- from the locale \isa{order{\isacharunderscore}preserving} are now active in \isa{lattice{\isacharunderscore}hom}, for example - \isa{le{\isacharprime}{\isachardot}less{\isacharunderscore}le{\isacharunderscore}trans}: + \isa{lat{\isacharprime}{\isachardot}less{\isacharunderscore}le{\isacharunderscore}trans}: \isa{{\isasymlbrakk}{\isacharquery}x\ {\isasymprec}\ {\isacharquery}y{\isacharsemicolon}\ {\isacharquery}y\ {\isasympreceq}\ {\isacharquery}z{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}x\ {\isasymprec}\ {\isacharquery}z}% \end{isamarkuptext}% \isamarkuptrue% diff -r 96cf8edb6249 -r 62e0f892e525 doc-src/TutorialI/Documents/document/Documents.tex --- a/doc-src/TutorialI/Documents/document/Documents.tex Thu Jan 01 21:28:38 2009 +0100 +++ b/doc-src/TutorialI/Documents/document/Documents.tex Thu Jan 01 21:30:13 2009 +0100 @@ -391,7 +391,7 @@ session is derived from a single parent, usually an object-logic image like \texttt{HOL}. This results in an overall tree structure, which is reflected by the output location in the file system - (usually rooted at \verb,~/isabelle/browser_info,). + (usually rooted at \verb,~/.isabelle/browser_info,). \medskip The easiest way to manage Isabelle sessions is via \texttt{isabelle mkdir} (generates an initial session source setup) diff -r 96cf8edb6249 -r 62e0f892e525 doc-src/TutorialI/Types/document/Numbers.tex --- a/doc-src/TutorialI/Types/document/Numbers.tex Thu Jan 01 21:28:38 2009 +0100 +++ b/doc-src/TutorialI/Types/document/Numbers.tex Thu Jan 01 21:30:13 2009 +0100 @@ -3,7 +3,6 @@ \def\isabellecontext{Numbers}% % \isadelimtheory -\isanewline % \endisadelimtheory %