src/HOL/ex/meson.ML
 changeset 1820 e381e1c51689 parent 1764 69b93ffc29ec child 2031 03a843f0f447
```--- a/src/HOL/ex/meson.ML	Fri Jun 21 11:57:00 1996 +0200
+++ b/src/HOL/ex/meson.ML	Fri Jun 21 12:18:50 1996 +0200
@@ -16,7 +16,7 @@
(*Prove theorems using fast_tac*)
fun prove_fun s =
prove_goal HOL.thy s
-         (fn prems => [ cut_facts_tac prems 1, fast_tac HOL_cs 1 ]);
+         (fn prems => [ cut_facts_tac prems 1, Fast_tac 1 ]);

(**** Negation Normal Form ****)

@@ -63,7 +63,7 @@
val [major] = goal HOL.thy
"! x. ? y. Q x y ==> ? f. ! x. Q x (f x)";
by (cut_facts_tac [major] 1);
-by (fast_tac (HOL_cs addEs [selectI]) 1);
+by (fast_tac (!claset addEs [selectI]) 1);
qed "choice";

@@ -430,7 +430,7 @@

(*First, breaks the goal into independent units*)
val safe_best_meson_tac =
-     SELECT_GOAL (TRY (safe_tac HOL_cs) THEN
+     SELECT_GOAL (TRY (safe_tac (!claset)) THEN
TRYALL (best_meson_tac size_of_subgoals));

(** Depth-first search version **)
@@ -464,7 +464,7 @@
(prolog_step_tac' (make_horns cls))));

val safe_meson_tac =
-     SELECT_GOAL (TRY (safe_tac HOL_cs) THEN
+     SELECT_GOAL (TRY (safe_tac (!claset)) THEN
TRYALL (iter_deepen_meson_tac));

```