1998 @{code Iff} (fm_of_term vs t1, fm_of_term vs t2) |
1998 @{code Iff} (fm_of_term vs t1, fm_of_term vs t2) |
1999 | fm_of_term vs (@{term "op &"} $ t1 $ t2) = @{code And} (fm_of_term vs t1, fm_of_term vs t2) |
1999 | fm_of_term vs (@{term "op &"} $ t1 $ t2) = @{code And} (fm_of_term vs t1, fm_of_term vs t2) |
2000 | fm_of_term vs (@{term "op |"} $ t1 $ t2) = @{code Or} (fm_of_term vs t1, fm_of_term vs t2) |
2000 | fm_of_term vs (@{term "op |"} $ t1 $ t2) = @{code Or} (fm_of_term vs t1, fm_of_term vs t2) |
2001 | fm_of_term vs (@{term "op -->"} $ t1 $ t2) = @{code Imp} (fm_of_term vs t1, fm_of_term vs t2) |
2001 | fm_of_term vs (@{term "op -->"} $ t1 $ t2) = @{code Imp} (fm_of_term vs t1, fm_of_term vs t2) |
2002 | fm_of_term vs (@{term "Not"} $ t') = @{code NOT} (fm_of_term vs t') |
2002 | fm_of_term vs (@{term "Not"} $ t') = @{code NOT} (fm_of_term vs t') |
2003 | fm_of_term vs (Const ("Ex", _) $ Abs (xn, xT, p)) = |
2003 | fm_of_term vs (Const (@{const_name "Ex"}, _) $ Abs (xn, xT, p)) = |
2004 @{code E} (fm_of_term (("", dummyT) :: vs) p) |
2004 @{code E} (fm_of_term (("", dummyT) :: vs) p) |
2005 | fm_of_term vs (Const ("All", _) $ Abs (xn, xT, p)) = |
2005 | fm_of_term vs (Const (@{const_name "All"}, _) $ Abs (xn, xT, p)) = |
2006 @{code A} (fm_of_term (("", dummyT) :: vs) p) |
2006 @{code A} (fm_of_term (("", dummyT) :: vs) p) |
2007 | fm_of_term vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term @{context} t); |
2007 | fm_of_term vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term @{context} t); |
2008 |
2008 |
2009 fun term_of_num vs (@{code C} i) = @{term "real :: int \<Rightarrow> real"} $ HOLogic.mk_number HOLogic.intT i |
2009 fun term_of_num vs (@{code C} i) = @{term "real :: int \<Rightarrow> real"} $ HOLogic.mk_number HOLogic.intT i |
2010 | term_of_num vs (@{code Bound} n) = Free (nth vs n) |
2010 | term_of_num vs (@{code Bound} n) = Free (nth vs n) |