Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned whitespace;
authorwenzelm
Thu, 28 Aug 2025 13:49:52 +0200
changeset 83064 08ad23c75b88
parent 83063 f8f82da1e560
child 83065 0a1a054d9b23
tuned whitespace;
src/Pure/Isar/specification.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/specification.ML	Wed Aug 27 20:42:15 2025 +0200
+++ b/src/Pure/Isar/specification.ML	Thu Aug 28 13:49:52 2025 +0200
@@ -260,7 +260,8 @@
       |> Local_Theory.define_internal ((b, mx), ((Binding.suffix_name "_raw" name, []), rhs));
 
     val ([(def_name, [th])], lthy3) = lthy2
-      |> Local_Theory.notes [((name, Code.singleton_default_equation_attrib :: atts), [([prove lthy2 raw_th], [])])];
+      |> Local_Theory.notes
+          [((name, Code.singleton_default_equation_attrib :: atts), [([prove lthy2 raw_th], [])])];
 
     val lthy4 = lthy3
       |> Spec_Rules.add name Spec_Rules.equational [lhs] [th];
isabelle