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/Lambda/ParRed.thy
changeset 19363 667b5ea637dd
parent 19086 1b3780be6cc2
child 20503 503ac4c5ef91 
--- a/src/HOL/Lambda/ParRed.thy	Sat Apr 08 22:12:02 2006 +0200
+++ b/src/HOL/Lambda/ParRed.thy	Sat Apr 08 22:51:06 2006 +0200
@@ -17,9 +17,9 @@
 consts
   par_beta :: "(dB \<times> dB) set"
 
-abbreviation (output)
+abbreviation
   par_beta_red :: "[dB, dB] => bool"  (infixl "=>" 50)
-  "(s => t) = ((s, t) \<in> par_beta)"
+  "s => t == (s, t) \<in> par_beta"
 
 inductive par_beta
   intros
isabelle