# HG changeset patch
# User wenzelm
# Date 1286829757 -3600
# Node ID c7f3efe59e4e1aec67401a03725035ff4d2c6d91
# Parent  3eb0694e6fcb8a250937a6ccff5cedc5cdc9e655
more examples;

diff -r 3eb0694e6fcb -r c7f3efe59e4e doc-src/IsarImplementation/Thy/Proof.thy
--- a/doc-src/IsarImplementation/Thy/Proof.thy	Mon Oct 11 21:10:50 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Proof.thy	Mon Oct 11 21:42:37 2010 +0100
@@ -52,11 +52,25 @@
   operation of exporting results from a context: a type variable
   @{text "\<alpha>"} is considered fixed as long as it occurs in some fixed
   term variable of the context.  For example, exporting @{text "x:
-  term, \<alpha>: type \<turnstile> x\<^isub>\<alpha> = x\<^isub>\<alpha>"} produces in the first step
-  @{text "x: term \<turnstile> x\<^isub>\<alpha> = x\<^isub>\<alpha>"} for fixed @{text "\<alpha>"},
-  and only in the second step @{text "\<turnstile> ?x\<^isub>?\<^isub>\<alpha> =
-  ?x\<^isub>?\<^isub>\<alpha>"} for schematic @{text "?x"} and @{text "?\<alpha>"}.
+  term, \<alpha>: type \<turnstile> x\<^isub>\<alpha> \<equiv> x\<^isub>\<alpha>"} produces in the first step @{text "x: term
+  \<turnstile> x\<^isub>\<alpha> \<equiv> x\<^isub>\<alpha>"} for fixed @{text "\<alpha>"}, and only in the second step
+  @{text "\<turnstile> ?x\<^isub>?\<^isub>\<alpha> \<equiv> ?x\<^isub>?\<^isub>\<alpha>"} for schematic @{text "?x"} and @{text "?\<alpha>"}.
+  The following Isar source text illustrates this scenario.
+*}
 
+example_proof
+  {
+    fix x  -- {* all potential occurrences of some @{text "x::\<tau>"} are fixed *}
+    {
+      have "x::'a \<equiv> x"  -- {* implicit type assigment by concrete occurrence *}
+        by (rule reflexive)
+    }
+    thm this  -- {* result still with fixed type @{text "'a"} *}
+  }
+  thm this  -- {* fully general result for arbitrary @{text "?x::?'a"} *}
+qed
+
+text {*
   \medskip The Isabelle/Isar proof context manages the gory details of
   term vs.\ type variables, with high-level principles for moving the
   frontier between fixed and schematic variables.