--- a/src/Doc/Isar_Ref/Synopsis.thy Sun Apr 24 20:37:24 2016 +0200
+++ b/src/Doc/Isar_Ref/Synopsis.thy Sun Apr 24 21:31:14 2016 +0200
@@ -26,7 +26,7 @@
assume "a = b" \<comment> \<open>type assignment at first occurrence in concrete term\<close>
txt \<open>Definitions (non-polymorphic):\<close>
- def x \<equiv> "t::'a"
+ define x :: 'a where "x = t"
txt \<open>Abbreviations (polymorphic):\<close>
let ?f = "\<lambda>x. x"
@@ -635,7 +635,7 @@
next
{
- def x \<equiv> t
+ define x where "x = t"
have "B x" \<proof>
}
have "B t" by fact