--- a/Sexp.ML Thu Aug 18 12:07:51 1994 +0200
+++ b/Sexp.ML Thu Aug 18 12:13:26 1994 +0200
@@ -1,7 +1,7 @@
(* Title: HOL/sexp
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1992 University of Cambridge
+ Copyright 1994 University of Cambridge
For sexp.thy. S-expressions.
*)
@@ -29,19 +29,19 @@
(** Sexp_case **)
-goalw Sexp.thy [Sexp_case_def] "Sexp_case(Leaf(a),c,d,e) = c(a)";
+goalw Sexp.thy [Sexp_case_def] "Sexp_case(c, d, e, Leaf(a)) = c(a)";
by (fast_tac (HOL_cs addIs [select_equality]
addSDs [Leaf_inject]
addSEs [Leaf_neq_Scons, Leaf_neq_Numb]) 1);
val Sexp_case_Leaf = result();
-goalw Sexp.thy [Sexp_case_def] "Sexp_case(Numb(k),c,d,e) = d(k)";
+goalw Sexp.thy [Sexp_case_def] "Sexp_case(c, d, e, Numb(k)) = d(k)";
by (fast_tac (HOL_cs addIs [select_equality]
addSDs [Numb_inject]
addSEs [Numb_neq_Scons, Numb_neq_Leaf]) 1);
val Sexp_case_Numb = result();
-goalw Sexp.thy [Sexp_case_def] "Sexp_case(M$N, c, d, e) = e(M,N)";
+goalw Sexp.thy [Sexp_case_def] "Sexp_case(c, d, e, M$N) = e(M,N)";
by (fast_tac (HOL_cs addIs [select_equality]
addSDs [Scons_inject]
addSEs [Scons_neq_Leaf, Scons_neq_Numb]) 1);
--- a/Sexp.thy Thu Aug 18 12:07:51 1994 +0200
+++ b/Sexp.thy Thu Aug 18 12:13:26 1994 +0200
@@ -10,11 +10,11 @@
consts
Sexp :: "'a node set set"
- Sexp_case :: "['a node set, 'a=>'b, nat=>'b, \
-\ ['a node set,'a node set]=>'b] => 'b"
+ Sexp_case :: "['a=>'b, nat=>'b, ['a node set, 'a node set]=>'b, \
+\ 'a node set] => 'b"
Sexp_rec :: "['a node set, 'a=>'b, nat=>'b, \
-\ ['a node set,'a node set,'b,'b]=>'b] => 'b"
+\ ['a node set, 'a node set, 'b, 'b]=>'b] => 'b"
pred_Sexp :: "('a node set * 'a node set)set"
@@ -22,7 +22,7 @@
Sexp_def "Sexp == lfp(%Z. range(Leaf) Un range(Numb) Un Z<*>Z)"
Sexp_case_def
- "Sexp_case(M,c,d,e) == @ z. (? x. M=Leaf(x) & z=c(x)) \
+ "Sexp_case(c,d,e,M) == @ z. (? x. M=Leaf(x) & z=c(x)) \
\ | (? k. M=Numb(k) & z=d(k)) \
\ | (? N1 N2. M = N1 $ N2 & z=e(N1,N2))"
@@ -31,6 +31,6 @@
Sexp_rec_def
"Sexp_rec(M,c,d,e) == wfrec(pred_Sexp, M, \
-\ %M g. Sexp_case(M, c, d, %N1 N2. e(N1, N2, g(N1), g(N2))))"
+\ %M g. Sexp_case(c, d, %N1 N2. e(N1, N2, g(N1), g(N2)), M))"
end