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/Induct/Term.thy
changeset 18461 9125d278fdc8
parent 16417 9bc16273c2d4
child 36862 952b2b102a0a 
--- a/src/HOL/Induct/Term.thy	Thu Dec 22 00:28:43 2005 +0100
+++ b/src/HOL/Induct/Term.thy	Thu Dec 22 00:28:44 2005 +0100
@@ -44,7 +44,7 @@
   assumes var: "!!v. P (Var v)"
     and app: "!!f ts. list_all P ts ==> P (App f ts)"
   shows term_induct2: "P t"
-and "list_all P ts"
+    and "list_all P ts"
   apply (induct t and ts)
      apply (rule var)
     apply (rule app)
isabelle