--- a/doc-src/IsarRef/conversion.tex Tue Sep 05 18:43:05 2000 +0200
+++ b/doc-src/IsarRef/conversion.tex Tue Sep 05 18:43:22 2000 +0200
@@ -21,8 +21,8 @@
% \texttt{} & & \\
\texttt{stac}~a~1 & & subst~a \\
\texttt{strip_tac}~1 & & intro~strip & \Text{(HOL)} \\
- \texttt{split_all_tac} & & simp~(no_asm_simp)~only: split_paired_all & \Text{(HOL)} \\
- & \approx & simp~only: split_tupled_all & \Text{(HOL)} \\
+ \texttt{split_all_tac} & & simp~(no_asm_simp)~only:~split_tupled_all & \Text{(HOL)} \\
+ & \approx & simp~only:~split_tupled_all & \Text{(HOL)} \\
& \ll & clarify & \Text{(HOL)} \\
\end{matharray}
--- a/src/FOL/cladata.ML Tue Sep 05 18:43:05 2000 +0200
+++ b/src/FOL/cladata.ML Tue Sep 05 18:43:22 2000 +0200
@@ -9,12 +9,7 @@
section "Classical Reasoner";
(*** Applying Make_Elim_Fun to create a classical "make_elim" rule ***)
-structure Make_Elim_Data =
-struct
- val classical = classical
-end;
-
-structure Make_Elim = Make_Elim_Fun (Make_Elim_Data);
+structure Make_Elim = Make_Elim_Fun(val classical = classical);
(*we don't redeclare the original make_elim (Tactic.make_elim) for
compatibliity with strange things done in many existing proofs *)
--- a/src/HOL/cladata.ML Tue Sep 05 18:43:05 2000 +0200
+++ b/src/HOL/cladata.ML Tue Sep 05 18:43:22 2000 +0200
@@ -32,12 +32,7 @@
(*** Applying Make_Elim_Fun to create a classical "make_elim" rule ***)
-structure Make_Elim_Data =
-struct
- val classical = classical
-end;
-
-structure Make_Elim = Make_Elim_Fun (Make_Elim_Data);
+structure Make_Elim = Make_Elim_Fun (val classical = classical);
(*we don't redeclare the original make_elim (Tactic.make_elim) for
compatibliity with strange things done in many existing proofs *)