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/CCL/ex/Nat.thy
changeset 60770 240563fbf41d
parent 58977 9576b510f6a2 
--- a/src/CCL/ex/Nat.thy	Thu Jul 23 14:20:51 2015 +0200
+++ b/src/CCL/ex/Nat.thy	Thu Jul 23 14:25:05 2015 +0200
@@ -3,7 +3,7 @@
     Copyright   1993  University of Cambridge
 *)
 
-section {* Programs defined over the natural numbers *}
+section \<open>Programs defined over the natural numbers\<close>
 
 theory Nat
 imports "../Wfd"
@@ -96,7 +96,7 @@
   done
 
 
-subsection {* Termination Conditions for Ackermann's Function *}
+subsection \<open>Termination Conditions for Ackermann's Function\<close>
 
 lemmas relI = NatPR_wf [THEN NatPR_wf [THEN lex_wf, THEN wfI]]
isabelle