--- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Thu Jan 04 15:29:44 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Thu Jan 04 17:11:09 2007 +0100
@@ -182,7 +182,7 @@
typedecl 'a foo
definition
- bar :: "'a foo \<Rightarrow> 'a \<Rightarrow> 'a"
+ bar :: "'a foo \<Rightarrow> 'a \<Rightarrow> 'a" where
"bar x y = y"
(*<*)
@@ -194,7 +194,7 @@
datatype 'a foo = Foo
definition
- bar :: "'a foo \<Rightarrow> 'a \<Rightarrow> 'a"
+ bar :: "'a foo \<Rightarrow> 'a \<Rightarrow> 'a" where
"bar x y = y"
(*>*)
@@ -212,7 +212,7 @@
(*>*)
definition
- pick_some :: "'a list \<Rightarrow> 'a"
+ pick_some :: "'a list \<Rightarrow> 'a" where
"pick_some xs = (SOME x. x \<in> set xs)"
(*<*)
@@ -221,7 +221,7 @@
setup {* Sign.parent_path *}
definition
- pick_some :: "'a list \<Rightarrow> 'a"
+ pick_some :: "'a list \<Rightarrow> 'a" where
"pick_some = hd"
(*>*)
@@ -655,7 +655,7 @@
*}
definition
- double_inc :: "int \<Rightarrow> int"
+ double_inc :: "int \<Rightarrow> int" where
"double_inc k = 2 * k + 1"
code_gen double_inc (SML "examples/integers.ML")
@@ -745,11 +745,11 @@
(*>*)
axclass eq \<subseteq> type
- attach "op ="
+ (attach "op =")
text {*
This merely introduces a class @{text eq} with corresponding
- operation @{const "op ="};
+ operation @{text "op ="};
the preprocessing framework does the rest.
*}
@@ -926,7 +926,7 @@
(SML "![]" and infixl 7 "::")
definition
- dummy_set :: "(nat \<Rightarrow> nat) set"
+ dummy_set :: "(nat \<Rightarrow> nat) set" where
"dummy_set = {Suc}"
text {*
@@ -946,7 +946,7 @@
*}
definition
- foobar_set :: "nat set"
+ foobar_set :: "nat set" where
"foobar_set = {0, 1, 2}"
text {*
@@ -1053,7 +1053,7 @@
*}
definition
- arbitrary_option :: "'a option"
+ arbitrary_option :: "'a option" where
[symmetric, code inline]: "arbitrary_option = arbitrary"
text {*
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Thu Jan 04 15:29:44 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Thu Jan 04 17:11:09 2007 +0100
@@ -225,7 +225,7 @@
\isanewline
\isacommand{definition}\isamarkupfalse%
\isanewline
-\ \ bar\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ foo\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\isanewline
+\ \ bar\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ foo\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}bar\ x\ y\ {\isacharequal}\ y{\isachardoublequoteclose}\isanewline
%
\isadelimML
@@ -266,7 +266,7 @@
\endisadelimML
\isacommand{definition}\isamarkupfalse%
\isanewline
-\ \ pick{\isacharunderscore}some\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\isanewline
+\ \ pick{\isacharunderscore}some\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}pick{\isacharunderscore}some\ xs\ {\isacharequal}\ {\isacharparenleft}SOME\ x{\isachardot}\ x\ {\isasymin}\ set\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimML
@@ -864,7 +864,7 @@
\isamarkuptrue%
\isacommand{definition}\isamarkupfalse%
\isanewline
-\ \ double{\isacharunderscore}inc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}int\ {\isasymRightarrow}\ int{\isachardoublequoteclose}\isanewline
+\ \ double{\isacharunderscore}inc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}int\ {\isasymRightarrow}\ int{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}double{\isacharunderscore}inc\ k\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ k\ {\isacharplus}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
@@ -981,7 +981,7 @@
\isanewline
\isacommand{axclass}\isamarkupfalse%
\ eq\ {\isasymsubseteq}\ type\isanewline
-\ \ \isakeyword{attach}\ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}%
+\ \ {\isacharparenleft}\isakeyword{attach}\ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}{\isacharparenright}%
\begin{isamarkuptext}%
This merely introduces a class \isa{eq} with corresponding
operation \isa{foo{\isachardot}op\ {\isacharequal}};
@@ -1351,7 +1351,7 @@
\isanewline
\isacommand{definition}\isamarkupfalse%
\isanewline
-\ \ dummy{\isacharunderscore}set\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}nat\ {\isasymRightarrow}\ nat{\isacharparenright}\ set{\isachardoublequoteclose}\isanewline
+\ \ dummy{\isacharunderscore}set\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}nat\ {\isasymRightarrow}\ nat{\isacharparenright}\ set{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}dummy{\isacharunderscore}set\ {\isacharequal}\ {\isacharbraceleft}Suc{\isacharbraceright}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
Then code generation for \isa{dummy{\isacharunderscore}set} will fail.
@@ -1371,7 +1371,7 @@
\isamarkuptrue%
\isacommand{definition}\isamarkupfalse%
\isanewline
-\ \ foobar{\isacharunderscore}set\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ set{\isachardoublequoteclose}\isanewline
+\ \ foobar{\isacharunderscore}set\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ set{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}foobar{\isacharunderscore}set\ {\isacharequal}\ {\isacharbraceleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbraceright}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
In this case the serializer would complain that \isa{insert}
@@ -1513,7 +1513,7 @@
\isamarkuptrue%
\isacommand{definition}\isamarkupfalse%
\isanewline
-\ \ arbitrary{\isacharunderscore}option\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ option{\isachardoublequoteclose}\isanewline
+\ \ arbitrary{\isacharunderscore}option\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ option{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isacharbrackleft}symmetric{\isacharcomma}\ code\ inline{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}arbitrary{\isacharunderscore}option\ {\isacharequal}\ arbitrary{\isachardoublequoteclose}%
\begin{isamarkuptext}%
By that, we replace any \isa{arbitrary} with option type
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs Thu Jan 04 15:29:44 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs Thu Jan 04 17:11:09 2007 +0100
@@ -2,11 +2,10 @@
import qualified Nat
class Null a where
- null :: a
+ nulla :: a
-head :: (Codegen.Null a_1) => [a_1] -> a_1
-head (y : xs) = y
-head [] = Codegen.null
+heada :: (Codegen.Null a) => ([a] -> a)
+heada (y : xs) = y
null_option :: Maybe b
null_option = Nothing
@@ -15,4 +14,4 @@
null = Codegen.null_option
dummy :: Maybe Nat.Nat
-dummy = Codegen.head [Just (Nat.Suc Nat.Zero_nat), Nothing]
+dummy = Codegen.heada [Just (Nat.Suc Nat.Zero_nat), Nothing]
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/arbitrary.ML Thu Jan 04 15:29:44 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/arbitrary.ML Thu Jan 04 17:11:09 2007 +0100
@@ -6,8 +6,7 @@
val arbitrary_option : 'a option = NONE;
-fun dummy_option [] = arbitrary_option
- | dummy_option (x :: xs) = SOME x;
+fun dummy_option [] = arbitrary_option;
end; (*struct Codegen*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_infix.ML Thu Jan 04 15:29:44 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_infix.ML Thu Jan 04 17:11:09 2007 +0100
@@ -4,8 +4,7 @@
structure HOL =
struct
-fun nota false = true
- | nota true = false;
+fun nota false = true;
end; (*struct HOL*)
@@ -14,9 +13,7 @@
datatype nat = Zero_nat | Suc of nat;
-fun less_nat Zero_nat (Suc n) = true
- | less_nat n Zero_nat = false
- | less_nat (Suc m) (Suc n) = less_nat m n;
+fun less_nat Zero_nat (Suc n) = true;
fun less_eq_nat m n = HOL.nota (less_nat n m);
@@ -25,7 +22,9 @@
structure Codegen =
struct
-fun in_interval (k, l) n = Nat.less_eq_nat k n andalso Nat.less_eq_nat n l;
+fun in_interval (k, l) n = (Nat.less_eq_nat k n andalso Nat.less_eq_nat n l)
+ | in_interval (k, l) n =
+ (Nat.less_eq_nat k n andalso Nat.less_eq_nat n l);
end; (*struct Codegen*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_literal.ML Thu Jan 04 15:29:44 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_literal.ML Thu Jan 04 17:11:09 2007 +0100
@@ -6,13 +6,9 @@
datatype boola = True | False;
-fun nota False = True
- | nota True = False;
+fun nota False = True;
-fun op_conj y True = y
- | op_conj x False = False
- | op_conj True y = y
- | op_conj False x = False;
+fun op_conj y True = y;
end; (*struct HOL*)
@@ -21,9 +17,7 @@
datatype nat = Zero_nat | Suc of nat;
-fun less_nat Zero_nat (Suc n) = HOL.True
- | less_nat n Zero_nat = HOL.False
- | less_nat (Suc m) (Suc n) = less_nat m n;
+fun less_nat Zero_nat (Suc n) = HOL.True;
fun less_eq_nat m n = HOL.nota (less_nat n m);
@@ -33,7 +27,9 @@
struct
fun in_interval (k, l) n =
- HOL.op_conj (Nat.less_eq_nat k n) (Nat.less_eq_nat n l);
+ HOL.op_conj (Nat.less_eq_nat k n) (Nat.less_eq_nat n l)
+ | in_interval (k, l) n =
+ HOL.op_conj (Nat.less_eq_nat k n) (Nat.less_eq_nat n l);
end; (*struct Codegen*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_mlbool.ML Thu Jan 04 15:29:44 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_mlbool.ML Thu Jan 04 17:11:09 2007 +0100
@@ -4,8 +4,7 @@
structure HOL =
struct
-fun nota false = true
- | nota true = false;
+fun nota false = true;
end; (*struct HOL*)
@@ -14,9 +13,7 @@
datatype nat = Zero_nat | Suc of nat;
-fun less_nat Zero_nat (Suc n) = true
- | less_nat n Zero_nat = false
- | less_nat (Suc m) (Suc n) = less_nat m n;
+fun less_nat Zero_nat (Suc n) = true;
fun less_eq_nat m n = HOL.nota (less_nat n m);
@@ -26,7 +23,9 @@
struct
fun in_interval (k, l) n =
- (Nat.less_eq_nat k n) andalso (Nat.less_eq_nat n l);
+ (Nat.less_eq_nat k n) andalso (Nat.less_eq_nat n l)
+ | in_interval (k, l) n =
+ (Nat.less_eq_nat k n) andalso (Nat.less_eq_nat n l);
end; (*struct Codegen*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML Thu Jan 04 15:29:44 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML Thu Jan 04 17:11:09 2007 +0100
@@ -14,12 +14,11 @@
type 'a null = {null_ : 'a};
fun null (A_:'a null) = #null_ A_;
-fun head (A_1_:'a_1 null) (y :: xs) = y
- | head (A_1_:'a_1 null) [] = null A_1_;
+fun head (A_:'a null) (y :: xs) = y;
val null_option : 'b option = NONE;
-fun null_optiona () = {null_ = null_option} : ('b option) null
+fun null_optiona () = {null_ = null_option} : ('b option) null ;;
val dummy : Nat.nat option =
head (null_optiona ()) [SOME (Nat.Suc Nat.Zero_nat), NONE];
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML Thu Jan 04 15:29:44 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML Thu Jan 04 17:11:09 2007 +0100
@@ -12,9 +12,8 @@
structure List =
struct
-fun memberl (A_1_:'a_1 Code_Generator.eq) x (y :: ys) =
- Code_Generator.op_eq A_1_ x y orelse memberl A_1_ x ys
- | memberl (A_1_:'a_1 Code_Generator.eq) x [] = false;
+fun memberl (A_:'a Code_Generator.eq) x (y :: ys) =
+ (Code_Generator.op_eq A_ x y orelse memberl A_ x ys);
end; (*struct List*)
@@ -25,8 +24,7 @@
(if List.memberl A_ z xs
then (if List.memberl A_ z ys then collect_duplicates A_ xs ys zs
else collect_duplicates A_ xs (z :: ys) zs)
- else collect_duplicates A_ (z :: xs) (z :: ys) zs)
- | collect_duplicates (A_:'a Code_Generator.eq) y ys [] = y;
+ else collect_duplicates A_ (z :: xs) (z :: ys) zs);
end; (*struct Codegen*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/dirty_set.ML Thu Jan 04 15:29:44 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/dirty_set.ML Thu Jan 04 17:11:09 2007 +0100
@@ -11,11 +11,11 @@
structure Codegen =
struct
-val dummy_set : (Nat.nat -> Nat.nat) list = Nat.Suc :: [];
+val dummy_set : (Nat.nat -> Nat.nat) list = (Nat.Suc :: []);
val foobar_set : Nat.nat list =
- Nat.Zero_nat ::
- (Nat.Suc Nat.Zero_nat :: (Nat.Suc (Nat.Suc Nat.Zero_nat) :: []));
+ (Nat.Zero_nat ::
+ (Nat.Suc Nat.Zero_nat :: (Nat.Suc (Nat.Suc Nat.Zero_nat) :: [])));
end; (*struct Codegen*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML Thu Jan 04 15:29:44 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML Thu Jan 04 17:11:09 2007 +0100
@@ -7,18 +7,16 @@
datatype nat = Zero_nat | Suc of nat;
fun plus_nat (Suc m) n = plus_nat m (Suc n)
- | plus_nat Zero_nat y = y;
+ | plus_nat (Suc m) n = Suc (plus_nat m n);
-fun times_nat (Suc m) n = plus_nat n (times_nat m n)
- | times_nat Zero_nat n = Zero_nat;
+fun times_nat (Suc m) n = plus_nat n (times_nat m n);
end; (*struct Nat*)
structure Codegen =
struct
-fun fac (Nat.Suc n) = Nat.times_nat (Nat.Suc n) (fac n)
- | fac Nat.Zero_nat = Nat.Suc Nat.Zero_nat;
+fun fac (Nat.Suc n) = Nat.times_nat (Nat.Suc n) (fac n);
end; (*struct Codegen*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML Thu Jan 04 15:29:44 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML Thu Jan 04 17:11:09 2007 +0100
@@ -7,10 +7,9 @@
datatype nat = Zero_nat | Suc of nat;
fun plus_nat (Suc m) n = plus_nat m (Suc n)
- | plus_nat Zero_nat y = y;
+ | plus_nat (Suc m) n = Suc (plus_nat m n);
-fun times_nat (Suc m) n = plus_nat n (times_nat m n)
- | times_nat Zero_nat n = Zero_nat;
+fun times_nat (Suc m) n = plus_nat n (times_nat m n);
end; (*struct Nat*)
@@ -19,7 +18,8 @@
fun fac n =
(case n of Nat.Zero_nat => Nat.Suc Nat.Zero_nat
- | Nat.Suc ma => Nat.times_nat n (fac ma));
+ | Nat.Suc m => Nat.times_nat n (fac m))
+ | fac (Nat.Suc n) = Nat.times_nat (Nat.Suc n) (fac n);
end; (*struct Codegen*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/integers.ML Thu Jan 04 15:29:44 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/integers.ML Thu Jan 04 17:11:09 2007 +0100
@@ -4,8 +4,8 @@
structure Codegen =
struct
-fun double_inc a =
- IntInf.+ ((IntInf.* ((2 : IntInf.int), a)), (1 : IntInf.int));
+val double_inc : IntInf.int -> IntInf.int =
+ (fn k => IntInf.+ ((IntInf.* ((2 : IntInf.int), k)), (1 : IntInf.int)));
end; (*struct Codegen*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML Thu Jan 04 15:29:44 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML Thu Jan 04 17:11:09 2007 +0100
@@ -14,7 +14,7 @@
fun op_eq_prod (A_:'a Code_Generator.eq) (B_:'b Code_Generator.eq) (x1, y1)
(x2, y2) =
- Code_Generator.op_eq A_ x1 x2 andalso Code_Generator.op_eq B_ y1 y2;
+ (Code_Generator.op_eq A_ x1 x2 andalso Code_Generator.op_eq B_ y1 y2);
end; (*struct Product_Type*)
@@ -33,18 +33,18 @@
fun less_prod (B_:'b Code_Generator.eq * 'b Orderings.ord)
(C_:'c Code_Generator.eq * 'c Orderings.ord) p1 p2 =
let
- val (x1a, y1a) = p1;
- val (x2a, y2a) = p2;
+ val (x1, y1) = p1;
+ val (x2, y2) = p2;
in
- Orderings.less (#2 B_) x1a x2a orelse
- Code_Generator.op_eq (#1 B_) x1a x2a andalso
- Orderings.less (#2 C_) y1a y2a
+ (Orderings.less (#2 B_) x1 x2 orelse
+ Code_Generator.op_eq (#1 B_) x1 x2 andalso
+ Orderings.less (#2 C_) y1 y2)
end;
fun less_eq_prod (B_:'b Code_Generator.eq * 'b Orderings.ord)
(C_:'c Code_Generator.eq * 'c Orderings.ord) p1 p2 =
- less_prod ((#1 B_), (#2 B_)) ((#1 C_), (#2 C_)) p1 p2 orelse
- Product_Type.op_eq_prod (#1 B_) (#1 C_) p1 p2;
+ (less_prod ((#1 B_), (#2 B_)) ((#1 C_), (#2 C_)) p1 p2 orelse
+ Product_Type.op_eq_prod (#1 B_) (#1 C_) p1 p2);
end; (*struct Codegen*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/lookup.ML Thu Jan 04 15:29:44 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/lookup.ML Thu Jan 04 17:11:09 2007 +0100
@@ -5,8 +5,7 @@
struct
fun lookup ((k, v) :: xs) l =
- (if ((k : string) = l) then SOME v else lookup xs l)
- | lookup [] l = NONE;
+ (if ((k : string) = l) then SOME v else lookup xs l);
end; (*struct Codegen*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML Thu Jan 04 15:29:44 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML Thu Jan 04 17:11:09 2007 +0100
@@ -6,13 +6,9 @@
datatype nat = Zero_nat | Suc of nat;
-fun less_nat Zero_nat (Suc n) = true
- | less_nat n Zero_nat = false
- | less_nat (Suc m) (Suc n) = less_nat m n;
+fun less_nat Zero_nat (Suc n) = true;
-fun minus_nat (Suc m) (Suc n) = minus_nat m n
- | minus_nat Zero_nat n = Zero_nat
- | minus_nat y Zero_nat = y;
+fun minus_nat (Suc m) (Suc n) = minus_nat m n;
end; (*struct Nat*)
@@ -20,13 +16,7 @@
struct
fun pick ((k, v) :: xs) n =
- (if Nat.less_nat n k then v else pick xs (Nat.minus_nat n k))
- | pick (x :: xs) n =
- let
- val (ka, va) = x;
- in
- (if Nat.less_nat n ka then va else pick xs (Nat.minus_nat n ka))
- end;
+ (if Nat.less_nat n k then v else pick xs (Nat.minus_nat n k));
end; (*struct Codegen*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML Thu Jan 04 15:29:44 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML Thu Jan 04 17:11:09 2007 +0100
@@ -6,13 +6,9 @@
datatype nat = Zero_nat | Suc of nat;
-fun less_nat Zero_nat (Suc n) = true
- | less_nat n Zero_nat = false
- | less_nat (Suc m) (Suc n) = less_nat m n;
+fun less_nat Zero_nat (Suc n) = true;
-fun minus_nat (Suc m) (Suc n) = minus_nat m n
- | minus_nat Zero_nat n = Zero_nat
- | minus_nat y Zero_nat = y;
+fun minus_nat (Suc m) (Suc n) = minus_nat m n;
end; (*struct Nat*)