Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/HOLCF/IOA/Sequence.thy
changeset 74563 042041c0ebeb
parent 63549 b0d31c7def86 
--- a/src/HOL/HOLCF/IOA/Sequence.thy	Wed Oct 20 20:04:28 2021 +0200
+++ b/src/HOL/HOLCF/IOA/Sequence.thy	Wed Oct 20 20:25:33 2021 +0200
@@ -996,13 +996,13 @@
 \<close>
 
 method_setup Seq_case =
-  \<open>Scan.lift Args.embedded >> (fn s => fn ctxt => SIMPLE_METHOD' (Seq_case_tac ctxt s))\<close>
+  \<open>Scan.lift Parse.embedded >> (fn s => fn ctxt => SIMPLE_METHOD' (Seq_case_tac ctxt s))\<close>
 
 method_setup Seq_case_simp =
-  \<open>Scan.lift Args.embedded >> (fn s => fn ctxt => SIMPLE_METHOD' (Seq_case_simp_tac ctxt s))\<close>
+  \<open>Scan.lift Parse.embedded >> (fn s => fn ctxt => SIMPLE_METHOD' (Seq_case_simp_tac ctxt s))\<close>
 
 method_setup Seq_induct =
-  \<open>Scan.lift Args.embedded --
+  \<open>Scan.lift Parse.embedded --
     Scan.optional ((Scan.lift (Args.$$$ "simp" -- Args.colon) |-- Attrib.thms)) []
     >> (fn (s, rws) => fn ctxt => SIMPLE_METHOD' (Seq_induct_tac ctxt s rws))\<close>
 
@@ -1010,10 +1010,10 @@
   \<open>Scan.succeed (SIMPLE_METHOD' o Seq_Finite_induct_tac)\<close>
 
 method_setup pair =
-  \<open>Scan.lift Args.embedded >> (fn s => fn ctxt => SIMPLE_METHOD' (pair_tac ctxt s))\<close>
+  \<open>Scan.lift Parse.embedded >> (fn s => fn ctxt => SIMPLE_METHOD' (pair_tac ctxt s))\<close>
 
 method_setup pair_induct =
-  \<open>Scan.lift Args.embedded --
+  \<open>Scan.lift Parse.embedded --
     Scan.optional ((Scan.lift (Args.$$$ "simp" -- Args.colon) |-- Attrib.thms)) []
     >> (fn (s, rws) => fn ctxt => SIMPLE_METHOD' (pair_induct_tac ctxt s rws))\<close>
isabelle