--- 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);