# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1329615227 0
# Node ID f223f8223d4a5a15280a16e3c194ef4ec3c5b90e
# Parent  231ec0c45bff25c1ef49a64d53e07303af2654e4
updated to new Isabelle

diff -r 231ec0c45bff -r f223f8223d4a ProgTutorial/Essential.thy
--- a/ProgTutorial/Essential.thy	Wed Feb 15 14:52:03 2012 +0000
+++ b/ProgTutorial/Essential.thy	Sun Feb 19 01:33:47 2012 +0000
@@ -1470,10 +1470,10 @@
 
   Since certified terms are, unlike terms, abstract objects, we cannot
   pattern-match against them. However, we can construct them. For example
-  the function @{ML_ind capply in Thm} produces a certified application.
+  the function @{ML_ind apply in Thm} produces a certified application.
 
   @{ML_response_fake [display,gray]
-  "Thm.capply @{cterm \"P::nat \<Rightarrow> bool\"} @{cterm \"3::nat\"}"
+  "Thm.apply @{cterm \"P::nat \<Rightarrow> bool\"} @{cterm \"3::nat\"}"
   "P 3"}
 
   Similarly the function @{ML_ind list_comb in Drule} from the structure @{ML_struct Drule}
diff -r 231ec0c45bff -r f223f8223d4a ProgTutorial/Package/Ind_Prelims.thy
--- a/ProgTutorial/Package/Ind_Prelims.thy	Wed Feb 15 14:52:03 2012 +0000
+++ b/ProgTutorial/Package/Ind_Prelims.thy	Sun Feb 19 01:33:47 2012 +0000
@@ -59,7 +59,7 @@
 assumes "trcl R x y"
 shows "(\<And>x. P x x) \<Longrightarrow> (\<And>x y z. R x y \<Longrightarrow> P y z \<Longrightarrow> P x z) \<Longrightarrow> P x y"
 apply(atomize (full))
-apply(cut_tac prems)
+apply(cut_tac assms)
 apply(unfold trcl_def)
 apply(drule spec[where x=P])
 apply(assumption)
@@ -211,7 +211,7 @@
 assumes "even n"
 shows "P 0 \<Longrightarrow> (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n"
 apply(atomize (full))
-apply(cut_tac prems)
+apply(cut_tac assms)
 apply(unfold even_def)
 apply(drule spec[where x=P])
 apply(drule spec[where x=Q])
diff -r 231ec0c45bff -r f223f8223d4a ProgTutorial/Tactical.thy
--- a/ProgTutorial/Tactical.thy	Wed Feb 15 14:52:03 2012 +0000
+++ b/ProgTutorial/Tactical.thy	Sun Feb 19 01:33:47 2012 +0000
@@ -2101,7 +2101,7 @@
   val add = @{cterm \"\<lambda>x y. x + (y::nat)\"}
   val two = @{cterm \"2::nat\"}
   val ten = @{cterm \"10::nat\"}
-  val ctrm = Thm.capply (Thm.capply add two) ten
+  val ctrm = Thm.apply (Thm.apply add two) ten
 in
   Thm.beta_conversion true ctrm
 end"
@@ -2119,7 +2119,7 @@
   val add = @{cterm \"\<lambda>x y. x + (y::nat)\"}
   val two = @{cterm \"2::nat\"}
   val ten = @{cterm \"10::nat\"}
-  val ctrm = Thm.capply (Thm.capply add two) ten
+  val ctrm = Thm.apply (Thm.apply add two) ten
 in
   Thm.prop_of (Thm.beta_conversion true ctrm)
 end"
@@ -2134,7 +2134,7 @@
    val add = @{cterm \"\<lambda>x y. x + (y::nat)\"}
    val two = @{cterm \"2::nat\"}
    val ten = @{cterm \"10::nat\"}
-   val ctrm = Thm.capply (Thm.capply add two) ten
+   val ctrm = Thm.apply (Thm.apply add two) ten
    val ctxt = @{context}
      |> Config.put eta_contract false 
      |> Config.put show_abbrevs false 
@@ -2187,7 +2187,7 @@
 "let
   val conv1 = Thm.beta_conversion false
   val conv2 = Conv.rewr_conv @{thm true_conj1}
-  val ctrm = Thm.capply @{cterm \"\<lambda>x. x \<and> False\"} @{cterm \"True\"}
+  val ctrm = Thm.apply @{cterm \"\<lambda>x. x \<and> False\"} @{cterm \"True\"}
 in
   (conv1 then_conv conv2) ctrm
 end"
diff -r 231ec0c45bff -r f223f8223d4a progtutorial.pdf
Binary file progtutorial.pdf has changed