--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs Wed Oct 24 21:12:44 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs Wed Oct 24 21:33:37 2007 +0200
@@ -6,7 +6,7 @@
nulla :: a;
};
-heada :: (Codegen.Null b) => [b] -> b;
+heada :: (Codegen.Null a) => [a] -> a;
heada (x : xs) = x;
heada [] = Codegen.nulla;
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML Wed Oct 24 21:12:44 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML Wed Oct 24 21:33:37 2007 +0200
@@ -11,8 +11,8 @@
type 'a null = {null : 'a};
fun null (A_:'a null) = #null A_;
-fun head B_ (x :: xs) = x
- | head B_ [] = null B_;
+fun head A_ (x :: xs) = x
+ | head A_ [] = null A_;
val null_option : 'a option = NONE;
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ocaml Wed Oct 24 21:12:44 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ocaml Wed Oct 24 21:33:37 2007 +0200
@@ -11,8 +11,8 @@
type 'a null = {null : 'a};;
let null _A = _A.null;;
-let rec head _B = function x :: xs -> x
- | [] -> null _B;;
+let rec head _A = function x :: xs -> x
+ | [] -> null _A;;
let rec null_option = None;;
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML Wed Oct 24 21:12:44 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML Wed Oct 24 21:33:37 2007 +0200
@@ -17,11 +17,11 @@
structure Codegen =
struct
-fun collect_duplicates B_ xs ys (z :: zs) =
- (if List.member B_ z xs
- then (if List.member B_ z ys then collect_duplicates B_ xs ys zs
- else collect_duplicates B_ xs (z :: ys) zs)
- else collect_duplicates B_ (z :: xs) (z :: ys) zs)
- | collect_duplicates B_ xs ys [] = xs;
+fun collect_duplicates A_ xs ys (z :: zs) =
+ (if List.member A_ z xs
+ then (if List.member 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_ xs ys [] = xs;
end; (*struct Codegen*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML Wed Oct 24 21:12:44 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML Wed Oct 24 21:33:37 2007 +0200
@@ -54,15 +54,15 @@
Branch of ('a, 'b) searchtree * 'a * ('a, 'b) searchtree |
Leaf of 'a * 'b;
-fun update (C1_, C2_) (it, entry) (Branch (t1, key, t2)) =
- (if HOL.less_eq ((Orderings.ord_order o Orderings.order_linorder) C2_)
+fun update (A1_, A2_) (it, entry) (Branch (t1, key, t2)) =
+ (if HOL.less_eq ((Orderings.ord_order o Orderings.order_linorder) A2_)
it key
- then Branch (update (C1_, C2_) (it, entry) t1, key, t2)
- else Branch (t1, key, update (C1_, C2_) (it, entry) t2))
- | update (C1_, C2_) (it, entry) (Leaf (key, vala)) =
- (if HOL.eqop C1_ it key then Leaf (key, entry)
+ then Branch (update (A1_, A2_) (it, entry) t1, key, t2)
+ else Branch (t1, key, update (A1_, A2_) (it, entry) t2))
+ | update (A1_, A2_) (it, entry) (Leaf (key, vala)) =
+ (if HOL.eqop A1_ it key then Leaf (key, entry)
else (if HOL.less_eq
- ((Orderings.ord_order o Orderings.order_linorder) C2_) it
+ ((Orderings.ord_order o Orderings.order_linorder) A2_) it
key
then Branch (Leaf (it, entry), it, Leaf (key, vala))
else Branch (Leaf (key, vala), it, Leaf (it, entry))));
--- a/doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex Wed Oct 24 21:12:44 2007 +0200
+++ b/doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex Wed Oct 24 21:33:37 2007 +0200
@@ -1303,7 +1303,7 @@
\ findzero{\isachardot}domintros%
\begin{isamarkuptext}%
\begin{isabelle}%
-{\isacharparenleft}{\isacharquery}f\ {\isacharquery}n\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ findzero{\isacharunderscore}dom\ {\isacharparenleft}{\isacharquery}f{\isacharcomma}\ Suc\ {\isacharquery}n{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ findzero{\isacharunderscore}dom\ {\isacharparenleft}{\isacharquery}f{\isacharcomma}\ {\isacharquery}n{\isacharparenright}%
+{\isacharparenleft}{\isadigit{0}}\ {\isacharless}\ {\isacharquery}f\ {\isacharquery}n\ {\isasymLongrightarrow}\ findzero{\isacharunderscore}dom\ {\isacharparenleft}{\isacharquery}f{\isacharcomma}\ Suc\ {\isacharquery}n{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ findzero{\isacharunderscore}dom\ {\isacharparenleft}{\isacharquery}f{\isacharcomma}\ {\isacharquery}n{\isacharparenright}%
\end{isabelle}
Domain introduction rules allow to show that a given value lies in the