dropped theory Term_Of_Syntax
authorhaftmann
Fri May 15 16:39:17 2009 +0200 (2009-05-15)
changeset 3118127304e12a412
parent 31180 dae7be64d614
child 31182 7ac0a57a57ed
dropped theory Term_Of_Syntax
src/HOL/IsaMakefile
src/HOL/ex/ROOT.ML
src/HOL/ex/Term_Of_Syntax.thy
     1.1 --- a/src/HOL/IsaMakefile	Fri May 15 16:39:16 2009 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri May 15 16:39:17 2009 +0200
     1.3 @@ -851,7 +851,7 @@
     1.4    ex/Recdefs.thy ex/Records.thy ex/ReflectionEx.thy			\
     1.5    ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy		\
     1.6    ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy \
     1.7 -  ex/Sudoku.thy ex/Tarski.thy ex/Term_Of_Syntax.thy	\
     1.8 +  ex/Sudoku.thy ex/Tarski.thy \
     1.9    ex/Termination.thy ex/Unification.thy ex/document/root.bib		\
    1.10    ex/document/root.tex ex/set.thy ex/svc_funcs.ML ex/svc_test.thy \
    1.11    ex/Predicate_Compile.thy ex/predicate_compile.ML ex/Predicate_Compile_ex.thy
     2.1 --- a/src/HOL/ex/ROOT.ML	Fri May 15 16:39:16 2009 +0200
     2.2 +++ b/src/HOL/ex/ROOT.ML	Fri May 15 16:39:17 2009 +0200
     2.3 @@ -11,7 +11,6 @@
     2.4    "Word",
     2.5    "Eval_Examples",
     2.6    "Quickcheck_Generators",
     2.7 -  "Term_Of_Syntax",
     2.8    "Codegenerator",
     2.9    "Codegenerator_Pretty",
    2.10    "NormalForm",
     3.1 --- a/src/HOL/ex/Term_Of_Syntax.thy	Fri May 15 16:39:16 2009 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,60 +0,0 @@
     3.4 -(*  Title:      HOL/ex/Term_Of_Syntax.thy
     3.5 -    ID:         $Id$
     3.6 -    Author:     Florian Haftmann, TU Muenchen
     3.7 -*)
     3.8 -
     3.9 -header {* Input syntax for term_of functions *}
    3.10 -
    3.11 -theory Term_Of_Syntax
    3.12 -imports Code_Eval
    3.13 -begin
    3.14 -
    3.15 -setup {*
    3.16 -  Sign.declare_const [] ((Binding.name "rterm_of", @{typ "'a \<Rightarrow> 'b"}), NoSyn)
    3.17 -  #> snd
    3.18 -*}
    3.19 -
    3.20 -notation (output)
    3.21 -  rterm_of ("\<guillemotleft>_\<guillemotright>")
    3.22 -
    3.23 -locale rterm_syntax =
    3.24 -  fixes rterm_of_syntax :: "'a \<Rightarrow> 'b" ("\<guillemotleft>_\<guillemotright>")
    3.25 -
    3.26 -parse_translation {*
    3.27 -let
    3.28 -  fun rterm_of_tr [t] = Lexicon.const @{const_name rterm_of} $ t
    3.29 -    | rterm_of_tr ts = raise TERM ("rterm_of_tr", ts);
    3.30 -in
    3.31 -  [(Syntax.fixedN ^ "rterm_of_syntax", rterm_of_tr)]
    3.32 -end
    3.33 -*}
    3.34 -
    3.35 -setup {*
    3.36 -let
    3.37 -  val subst_rterm_of = map_aterms
    3.38 -    (fn Free (v, _) => error ("illegal free variable in term quotation: " ^ quote v) | t => t)
    3.39 -      o HOLogic.reflect_term;
    3.40 -  fun subst_rterm_of' (Const (@{const_name rterm_of}, _), [t]) = subst_rterm_of t
    3.41 -    | subst_rterm_of' (Const (@{const_name rterm_of}, _), _) =
    3.42 -        error ("illegal number of arguments for " ^ quote @{const_name rterm_of})
    3.43 -    | subst_rterm_of' (t, ts) = list_comb (t, map (subst_rterm_of' o strip_comb) ts);
    3.44 -  fun subst_rterm_of'' t = 
    3.45 -    let
    3.46 -      val t' = subst_rterm_of' (strip_comb t);
    3.47 -    in if t aconv t'
    3.48 -      then NONE
    3.49 -      else SOME t'
    3.50 -    end;
    3.51 -  fun check_rterm_of ts ctxt =
    3.52 -    let
    3.53 -      val ts' = map subst_rterm_of'' ts;
    3.54 -    in if exists is_some ts'
    3.55 -      then SOME (map2 the_default ts ts', ctxt)
    3.56 -      else NONE
    3.57 -    end;
    3.58 -in
    3.59 -  Context.theory_map (Syntax.add_term_check 0 "rterm_of" check_rterm_of)
    3.60 -end;
    3.61 -*}
    3.62 -
    3.63 -end