# HG changeset patch
# User chaieb
# Date 1183730968 -7200
# Node ID e65e36dbe0d2fcbcc2bb7c42099373d7c887e558
# Parent  6a8fb529b5428cf944ece2f53331154dadd52b4d
Some examples for reifying type variables

diff -r 6a8fb529b542 -r e65e36dbe0d2 src/HOL/ex/ReflectionEx.thy
--- a/src/HOL/ex/ReflectionEx.thy	Fri Jul 06 16:09:27 2007 +0200
+++ b/src/HOL/ex/ReflectionEx.thy	Fri Jul 06 16:09:28 2007 +0200
@@ -37,12 +37,12 @@
 "interp e (Neg f) = (~ interp e f)" |
 "interp e (ExQ f) = (EX x. interp (x#e) f)"
 
-lemmas interp_reify_eqs = interp.simps[where ?'b = int]
-declare interp_reify_eqs(1)[reify add: interp_reify_eqs]
+lemmas interp_reify_eqs = interp.simps
+declare interp_reify_eqs[reify]
 
-lemma "EX x::int. y < x & x < z"
-  apply reify
-oops
+lemma "EX x. x < y & x < z"
+  apply (reify )
+  oops
 
 datatype fm = And fm fm | Or fm fm | Imp fm fm | Iff fm fm | NOT fm | At nat