diff options
Diffstat (limited to 'snapshots/isabelle/lib/lem/Lem_string_extra.thy')
| -rw-r--r-- | snapshots/isabelle/lib/lem/Lem_string_extra.thy | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/snapshots/isabelle/lib/lem/Lem_string_extra.thy b/snapshots/isabelle/lib/lem/Lem_string_extra.thy index bd8317ba..9991308f 100644 --- a/snapshots/isabelle/lib/lem/Lem_string_extra.thy +++ b/snapshots/isabelle/lib/lem/Lem_string_extra.thy @@ -1,14 +1,14 @@ -chapter \<open>Generated by Lem from string_extra.lem.\<close> +chapter \<open>Generated by Lem from \<open>string_extra.lem\<close>.\<close> theory "Lem_string_extra" -imports - Main - "Lem_num" - "Lem_list" - "Lem_basic_classes" - "Lem_string" - "Lem_list_extra" +imports + Main + "Lem_num" + "Lem_list" + "Lem_basic_classes" + "Lem_string" + "Lem_list_extra" begin @@ -43,7 +43,7 @@ fun stringFromNatHelper :: " nat \<Rightarrow>(char)list \<Rightarrow>(char)li if n =( 0 :: nat) then acc1 else - stringFromNatHelper (n div( 10 :: nat)) (char_of_nat ((n mod( 10 :: nat)) +( 48 :: nat)) # acc1))" + stringFromNatHelper (n div( 10 :: nat)) ((%n. char_of (n::nat)) ((n mod( 10 :: nat)) +( 48 :: nat)) # acc1))" (*val stringFromNat : nat -> string*) @@ -58,7 +58,7 @@ fun stringFromNaturalHelper :: " nat \<Rightarrow>(char)list \<Rightarrow>(cha if n =( 0 :: nat) then acc1 else - stringFromNaturalHelper (n div( 10 :: nat)) (char_of_nat ( ((n mod( 10 :: nat)) +( 48 :: nat))) # acc1))" + stringFromNaturalHelper (n div( 10 :: nat)) ((%n. char_of (n::nat)) ( ((n mod( 10 :: nat)) +( 48 :: nat))) # acc1))" (*val stringFromNatural : natural -> string*) @@ -98,7 +98,7 @@ definition nth :: " string \<Rightarrow> nat \<Rightarrow> char " where (*val stringConcat : list string -> string*) definition stringConcat :: "(string)list \<Rightarrow> string " where " stringConcat s = ( - List.foldr (op@) s (''''))" + List.foldr (@) s (''''))" (******************************************************************************) |