equal
deleted
inserted
replaced
43 |
43 |
44 "--------------------- NTH ---------------------------------------------------"; |
44 "--------------------- NTH ---------------------------------------------------"; |
45 "--------------------- NTH ---------------------------------------------------"; |
45 "--------------------- NTH ---------------------------------------------------"; |
46 "--------------------- NTH ---------------------------------------------------"; |
46 "--------------------- NTH ---------------------------------------------------"; |
47 val ctxt = Proof_Context.init_global @{theory} |
47 val ctxt = Proof_Context.init_global @{theory} |
48 val prog_expr = assoc_rls "prog_expr" |
48 val prog_expr = get_rls @{context} "prog_expr" |
49 |
49 |
50 val t = TermC.str2term "NTH 1 [a,b,c,d,e]"; |
50 val t = TermC.str2term "NTH 1 [a,b,c,d,e]"; |
51 TermC.atomty t; |
51 TermC.atomty t; |
52 val thm = Thm.prop_of @{thm NTH_NIL}; |
52 val thm = Thm.prop_of @{thm NTH_NIL}; |
53 TermC.atomty thm; |
53 TermC.atomty thm; |
79 else error "NTH 3 [a,b,c,d,e] = c ..changed"; |
79 else error "NTH 3 [a,b,c,d,e] = c ..changed"; |
80 |
80 |
81 "--------------------- Length ------------------------------------------------"; |
81 "--------------------- Length ------------------------------------------------"; |
82 "--------------------- Length ------------------------------------------------"; |
82 "--------------------- Length ------------------------------------------------"; |
83 "--------------------- Length ------------------------------------------------"; |
83 "--------------------- Length ------------------------------------------------"; |
84 val prog_expr = assoc_rls "prog_expr" |
84 val prog_expr = get_rls @{context} "prog_expr" |
85 |
85 |
86 val thy = @{theory ListC}; |
86 val thy = @{theory ListC}; |
87 val t = TermC.str2term "Length [1, 1, 1]"; |
87 val t = TermC.str2term "Length [1, 1, 1]"; |
88 val SOME (t, asm) = rewrite_ ctxt tless_true tval_rls false @{thm LENGTH_CONS} t; |
88 val SOME (t, asm) = rewrite_ ctxt tless_true tval_rls false @{thm LENGTH_CONS} t; |
89 UnparseC.term t = "1 + Length [1, 1]"; |
89 UnparseC.term t = "1 + Length [1, 1]"; |