--- a/src/Doc/Codegen/Refinement.thy Wed Feb 12 08:37:28 2014 +0100
+++ b/src/Doc/Codegen/Refinement.thy Wed Feb 12 08:37:28 2014 +0100
@@ -148,15 +148,15 @@
\noindent It is good style, although no absolute requirement, to
provide code equations for the original artefacts of the implemented
type, if possible; in our case, these are the datatype constructor
- @{const Queue} and the case combinator @{const queue_case}:
+ @{const Queue} and the case combinator @{const case_queue}:
*}
lemma %quote Queue_AQueue [code]:
"Queue = AQueue []"
by (simp add: AQueue_def fun_eq_iff)
-lemma %quote queue_case_AQueue [code]:
- "queue_case f (AQueue xs ys) = f (ys @ rev xs)"
+lemma %quote case_queue_AQueue [code]:
+ "case_queue f (AQueue xs ys) = f (ys @ rev xs)"
by (simp add: AQueue_def)
text {*
@@ -164,7 +164,7 @@
*}
text %quotetypewriter {*
- @{code_stmts empty enqueue dequeue Queue queue_case (SML)}
+ @{code_stmts empty enqueue dequeue Queue case_queue (SML)}
*}
text {*
@@ -274,4 +274,3 @@
*}
end
-
--- a/src/HOL/Decision_Procs/Cooper.thy Wed Feb 12 08:37:28 2014 +0100
+++ b/src/HOL/Decision_Procs/Cooper.thy Wed Feb 12 08:37:28 2014 +0100
@@ -303,12 +303,12 @@
lemma evaldjf_bound0:
assumes nb: "\<forall>x\<in> set xs. bound0 (f x)"
shows "bound0 (evaldjf f xs)"
- using nb by (induct xs) (auto simp add: evaldjf_def djf_def Let_def, case_tac "f x1", auto)
+ using nb by (induct xs) (auto simp add: evaldjf_def djf_def Let_def, case_tac "f a", auto)
lemma evaldjf_qf:
assumes nb: "\<forall>x\<in> set xs. qfree (f x)"
shows "qfree (evaldjf f xs)"
- using nb by (induct xs) (auto simp add: evaldjf_def djf_def Let_def, case_tac "f x1", auto)
+ using nb by (induct xs) (auto simp add: evaldjf_def djf_def Let_def, case_tac "f a", auto)
fun disjuncts :: "fm \<Rightarrow> fm list"
where
--- a/src/HOL/Decision_Procs/Ferrack.thy Wed Feb 12 08:37:28 2014 +0100
+++ b/src/HOL/Decision_Procs/Ferrack.thy Wed Feb 12 08:37:28 2014 +0100
@@ -328,12 +328,12 @@
lemma evaldjf_bound0:
assumes nb: "\<forall> x\<in> set xs. bound0 (f x)"
shows "bound0 (evaldjf f xs)"
- using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f x1", auto)
+ using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto)
lemma evaldjf_qf:
assumes nb: "\<forall> x\<in> set xs. qfree (f x)"
shows "qfree (evaldjf f xs)"
- using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f x1", auto)
+ using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto)
fun disjuncts :: "fm \<Rightarrow> fm list" where
"disjuncts (Or p q) = disjuncts p @ disjuncts q"
@@ -2030,4 +2030,3 @@
by rferrack
end
-
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Wed Feb 12 08:37:28 2014 +0100
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Wed Feb 12 08:37:28 2014 +0100
@@ -761,12 +761,12 @@
lemma evaldjf_bound0:
assumes nb: "\<forall> x\<in> set xs. bound0 (f x)"
shows "bound0 (evaldjf f xs)"
- using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f x1", auto)
+ using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto)
lemma evaldjf_qf:
assumes nb: "\<forall> x\<in> set xs. qfree (f x)"
shows "qfree (evaldjf f xs)"
- using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f x1", auto)
+ using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto)
fun disjuncts :: "fm \<Rightarrow> fm list" where
"disjuncts (Or p q) = (disjuncts p) @ (disjuncts q)"