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.
doc-src/TutorialI/Protocol/Message.thy
changeset 32960 69916a850301
parent 32265 fa8872f21ac3
child 35109 0015a0a99ae9 
--- a/doc-src/TutorialI/Protocol/Message.thy	Sat Oct 17 01:05:59 2009 +0200
+++ b/doc-src/TutorialI/Protocol/Message.thy	Sat Oct 17 14:43:18 2009 +0200
@@ -61,8 +61,8 @@
      msg = Agent  agent
          | Nonce  nat
          | Key    key
-	 | MPair  msg msg
-	 | Crypt  key msg
+         | MPair  msg msg
+         | Crypt  key msg
 
 text {*
 \noindent
@@ -855,8 +855,8 @@
     (Fake_insert_simp_tac ss 1
      THEN
      IF_UNSOLVED (Blast.depth_tac
-		  (cs addIs [analz_insertI,
-				   impOfSubs analz_subset_parts]) 4 1))
+                  (cs addIs [analz_insertI,
+                                   impOfSubs analz_subset_parts]) 4 1))
 
 fun spy_analz_tac (cs,ss) i =
   DETERM
isabelle