equal
deleted
inserted
replaced
150 val thy = @{theory (** )"Poly" ( **) Rational(**) (*required for rls "norm_Rational"*)} |
150 val thy = @{theory (** )"Poly" ( **) Rational(**) (*required for rls "norm_Rational"*)} |
151 val ctxt = Proof_Context.init_global thy |
151 val ctxt = Proof_Context.init_global thy |
152 val auto_script = |
152 val auto_script = |
153 Auto_Prog.gen thy @{term "ttt :: real"} (get_rls ctxt "norm_Rational"); |
153 Auto_Prog.gen thy @{term "ttt :: real"} (get_rls ctxt "norm_Rational"); |
154 writeln(UnparseC.term auto_script); |
154 writeln(UnparseC.term auto_script); |
155 TermC.atomty auto_script; |
155 TermC.atom_trace_detail @{context} auto_script; |
156 (*** |
156 (*** |
157 *** Const (Program.Stepwise, 'z => 'z => 'z) |
157 *** Const (Program.Stepwise, 'z => 'z => 'z) |
158 *** . Free (t_t, 'z) |
158 *** . Free (t_t, 'z) |
159 *** . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a) |
159 *** . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a) |
160 *** . . Const (Program.Try, ('a => 'a) => 'a => 'a) |
160 *** . . Const (Program.Try, ('a => 'a) => 'a => 'a) |